5 papers
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…
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…