research
∙
11/30/2021
SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs
Much recent research has been devoted to modeling effects within type th...
share
research
∙
03/17/2018
Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms
Scripting proofs with tactics has been a tradition in interactive theore...
research
∙
03/17/2018
Meta-F*: Metaprogramming and Tactics in an Effectful Program Verifier
Verification tools for effectful programming languages often rely on aut...
research
∙
11/17/2017
WYS*: A Verified Language Extension for Secure Multi-party Computations
Secure multi-party computation (MPC) enables a set of mutually distrusti...
research
∙
07/08/2017