112 citations · 183 across the 6 of their papers we have counts for
7 papers · 1 filter
SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs
Nikhil Swamy, Aseem Rastogi, Aymeric Fromherz +3
Much recent research has been devoted to modeling effects within type theory. Building on this work, we observe that effectful type theories can provide a foundation on which to bu…
Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms
Guido Martínez, Danel Ahman, Victor Dumitrescu +10
We introduce Meta-F*, a tactics and metaprogramming framework for the F* program verifier. The main novelty of Meta-F* is allowing the use of tactics and metaprogramming to dischar…
WYS*: A DSL for Verified Secure Multi-party Computations
Aseem Rastogi, Nikhil Swamy, Michael Hicks
Secure multi-party computation (MPC) enables a set of mutually distrusting parties to cooperatively compute, using a cryptographic protocol, a function over their private data. Thi…
Recalling a Witness: Foundations and Applications of Monotonic State
Danel Ahman, Cédric Fournet, Catalin Hritcu +3
We provide a way to ease the verification of programs whose state evolves monotonically. The main idea is that a property witnessed in a prior state can be soundly recalled in the…
A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
Niklas Grimm, Kenji Maillard, Cédric Fournet +7
Relational properties describe multiple runs of one or more programs. They characterize many useful notions of security, program refinement, and equivalence for programs with diver…
Verified Low-Level Programming Embedded in F*
Jonathan Protzenko, Jean-Karim Zinzindohoué, Aseem Rastogi +8
We present Low*, a language for low-level programming and verification, and its application to high-assurance optimized cryptographic libraries. Low* is a shallow embedding of a sm…
Polymonadic Programming
Michael Hicks, Gavin Bierman, Nataliya Guts +2
Monads are a popular tool for the working functional programmer to structure effectful computations. This paper presents polymonads, a generalization of monads. Polymonads give the…