10 papers · 1 filter
Propositional Equality for Gradual Dependently Typed Programming
Joseph Eremondi, Ronald Garcia, Éric Tanter
Gradual dependent types can help with the incremental adoption of dependently typed code by providing a principled semantics for imprecise types and proofs, where some parts have b…
Approximate Normalization and Eager Equality Checking for Gradual Inductive Families
Joseph Eremondi, Ronald Garcia, Éric Tanter
Harnessing the power of dependently typed languages can be difficult. Programmers must manually construct proofs to produce well-typed programs, which is not an easy task. In parti…
Gradual Program Analysis for Null Pointers
Sam Estep, Jenna Wise, Jonathan Aldrich +3
Static analysis tools typically address the problem of excessive false positives by requiring programmers to explicitly annotate their code. However, when faced with incomplete ann…
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…