Search

• < Previous
• 1
• Next >

---

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;]

---

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;]

---

On the Semantic Expressiveness of Iso- and Equi-Recursive Types

Dominique Devriese ; Eric Mark Martin ; Marco Patrignani.

Recursive types extend the simply-typed lambda calculus (STLC) with the additional expressive power to enable diverging computation and to encode recursive data-types (e.g., lists). Two formulations of recursive types exist: iso-recursive and equi-recursive. The relative advantages of iso- and&nbsp;[&hellip;]

---