research
∙
07/12/2022
Mechanizing Refinement Types (extended)
Practical checkers based on refinement types use the combination of impl...
share
research
∙
07/08/2022
Flux: Liquid Types for Rust
We introduce Flux, which shows how logical refinements can work hand in ...
research
∙
05/05/2021
Refinements of Futures Past: Higher-Order Specification with Implicit Refinement Types (Extended Version)
Refinement types decorate types with assertions that enable automatic ve...
research
∙
04/30/2021
Isolation Without Taxation: Near Zero Cost Transitions for SFI
Almost all SFI systems use heavyweight transitions that incur significan...
research
∙
04/01/2021
Solver-Aided Constant-Time Circuit Verification
We present Xenon, a solver-aided method for formally verifying that Veri...
research
∙
10/15/2020
Refinement Types: A Tutorial
Refinement types enrich a language's type system with logical predicates...
research
∙
05/01/2020
Automatically Eliminating Speculative Leaks With Blade
We introduce BLADE, a new approach to automatically and efficiently synt...
research
∙
11/11/2019
Program Synthesis by Type-Guided Abstraction Refinement
We consider the problem of type-directed component based synthesis where...
research
∙
10/07/2019
Iodine: Verifying Constant-Time Execution of Hardware
To be secure, cryptographic algorithms crucially rely on the underlying ...
research
∙
11/09/2017
Refinement Reflection: Complete Verification with SMT
We introduce Refinement Reflection, a new framework for building SMT-bas...
research
∙
08/25/2017
Learning to Blame: Localizing Novice Type Errors with Data-Driven Diagnosis
Localizing type errors is challenging in languages with global type infe...
research
∙
08/07/2017
Deriving Law-Abiding Instances
Liquid Haskell's refinement-reflection feature augments the Haskell lang...
research
∙
06/24/2017
Local Refinement Typing
We introduce the Fusion algorithm for local refinement type inference, y...
research
∙
07/04/2012