Search

• < Previous
• 1
• Next >

---

Transpension: The Right Adjoint to the Pi-type

Andreas Nuyts ; Dominique Devriese.

Presheaf models of dependent type theory have been successfully applied to model HoTT, parametricity, and directed, guarded and nominal type theory. There has been considerable interest in internalizing aspects of these presheaf models, either to make the resulting language more expressive, or in&nbsp;[&hellip;]

---

Modular, Fully-abstract Compilation by Approximate Back-translation

Dominique Devriese ; Marco Patrignani ; Frank Piessens ; Steven Keuchel.

A compiler is fully-abstract if the compilation from source language programs to target language programs reflects and preserves behavioural equivalence. Such compilers have important security benefits, as they limit the power of an attacker interacting with the program in the target language to&nbsp;[&hellip;]

---