3 papers
cs.PL2026
Misquoted No More: Securely Extracting F* Programs with IO
Cezar-Constantin Andrici, Abigail Pribisova, Danel Ahman +3
Shallow embeddings that use monads to represent effects are popular in proof-oriented languages because they are convenient for formal verification. Once shallowly embedded program…
cs.PL2025
SecRef*: Securely Sharing Mutable References Between Verified and Unverified Code in F*
Cezar-Constantin Andrici, Danel Ahman, Catalin Hritcu +4
We introduce SecRef*, a secure compilation framework protecting stateful programs verified in F* against linked unverified code, with which the program dynamically shares ML-style…
cs.LO2024
From Rewrite Rules to Axioms in the -Calculus Modulo Theory
Valentin Blot, Gilles Dowek, Thomas Traversié +1
The -calculus modulo theory is an extension of simply typed -calculus with dependent types and user-defined rewrite rules. We show that it is possible to replace the rewri…