18 citations · 75 across the 12 of their papers we have counts for
17 papers
Gradual Sensitivity Typing
Damian Arquez, Matías Toro, Éric Tanter
Reasoning about the sensitivity of functions with respect to their inputs has interesting applications in various areas, such as differential privacy. In order to check and enforce…
Gradual C0: Symbolic Execution for Gradual Verification
Jenna DiVincenzo, Ian McCormack, Hemant Gouni +7
Current static verification techniques support a wide range of programs. However, such techniques only support complete and detailed specifications, which places an undue burden on…
A Reasonably Gradual Type Theory
Kenji Maillard, Meven Lennon-Bertrand, Nicolas Tabareau +1
Gradualizing the Calculus of Inductive Constructions (CIC) involves dealing with subtle tensions between normalization, graduality, and conservativity with respect to CIC. Recently…
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…
The Multiverse: Logical Modularity for Proof Assistants
Kenji Maillard, Nicolas Margulies, Matthieu Sozeau +2
Proof assistants play a dual role as programming languages and logical systems. As programming languages, proof assistants offer standard modularity mechanisms such as first-class…
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…