research
∙
08/03/2023
Gradual Sensitivity Typing
Reasoning about the sensitivity of functions with respect to their input...
share
research
∙
03/02/2023
Securing Verified IO Programs Against Unverified Code in F*
We introduce SCIO*, a formally secure compilation framework for statical...
research
∙
10/05/2022
Gradual C0: Symbolic Execution for Efficient Gradual Verification
Current static verification techniques such as separation logic support ...
research
∙
09/02/2022
A Reasonably Gradual Type Theory
Gradualizing the Calculus of Inductive Constructions (CIC) involves deal...
research
∙
05/02/2022
Propositional Equality for Gradual Dependently Typed Programming
Gradual dependent types can help with the incremental adoption of depend...
research
∙
08/23/2021
The Multiverse: Logical Modularity for Proof Assistants
Proof assistants play a dual role as programming languages and logical s...
research
∙
07/10/2021
Approximate Normalization and Eager Equality Checking for Gradual Inductive Families
Harnessing the power of dependently typed languages can be difficult. Pr...
research
∙
05/13/2021
Gradual Program Analysis for Null Pointers
Static analysis tools typically address the problem of excessive false p...
research
∙
11/20/2020
Gradualizing the Calculus of Inductive Constructions
Acknowledging the ordeal of a fully formal development in a proof assist...
research
∙
10/21/2020
Contextual Linear Types for Differential Privacy
Language support for differentially-private programming is both crucial ...
research
∙
11/11/2019
Existential Types for Relaxed Noninterference
Information-flow security type systems ensure confidentiality by enforci...
research
∙
09/11/2019
The Marriage of Univalence and Parametricity
Reasoning modulo equivalences is natural for everyone, including mathema...
research
∙
07/11/2019
Trace-Relating Compiler Correctness and Secure Compilation
Compiler correctness is, in its simplest form, defined as the inclusion ...
research
∙
06/15/2019
Approximate Normalization for Gradual Dependent Types
Dependent types help programmers write highly reliable code. However, th...
research
∙
06/11/2019
Polymorphic Relaxed Noninterference
Information-flow security typing statically preserves confidentiality by...
research
∙
03/04/2019
Dijkstra Monads for All
This paper proposes a general semantic framework for verifying programs ...
research
∙
07/12/2018
Gradual Parametricity, Revisited (with Appendix)
Bringing the benefits of gradual typing to a language with parametric po...
research
∙
07/12/2018
Gradual Parametricity, Revisited
Bringing the benefits of gradual typing to a language with parametric po...
research
∙
07/05/2018