6 papers · 2 filters
Existential Types for Relaxed Noninterference
Raimil Cruz, Éric Tanter
Information-flow security type systems ensure confidentiality by enforcing noninterference: a program cannot leak private data to public channels. However, in practice, programs ne…
The Marriage of Univalence and Parametricity
Nicolas Tabareau, Éric Tanter, Matthieu Sozeau
Reasoning modulo equivalences is natural for everyone, including mathematicians. Unfortunately, in proof assistants based on type theory, equality is appallingly syntactic and, as…
Trace-Relating Compiler Correctness and Secure Compilation
Carmine Abate, Roberto Blanco, Stefan Ciobaca +6
Compiler correctness is, in its simplest form, defined as the inclusion of the set of traces of the compiled program into the set of traces of the original program, which is equiva…
Approximate Normalization for Gradual Dependent Types
Joseph Eremondi, Éric Tanter, Ronald Garcia
Dependent types help programmers write highly reliable code. However, this reliability comes at a cost: it can be challenging to write new prototypes in (or migrate old code to) de…
Polymorphic Relaxed Noninterference
Raimil Cruz, Éric Tanter
Information-flow security typing statically preserves confidentiality by enforcing noninterference. To address the practical need of selective and flexible declassification of conf…
Dijkstra Monads for All
Kenji Maillard, Danel Ahman, Robert Atkey +4
This paper proposes a general semantic framework for verifying programs with arbitrary monadic side-effects using Dijkstra monads, which we define as monad-like structures indexed…