6 papers
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…
Strong Normalisation for Asynchronous Effects
Danel Ahman, Ilja Sobolev
Asynchronous effects of Ahman and Pretnar complement the conventional synchronous treatment of algebraic effects with asynchrony based on decoupling the execution of algebraic oper…
Sheaves as oracle computations
Danel Ahman, Andrej Bauer
In type theory, an oracle may be specified abstractly by a predicate whose domain is the type of queries asked of the oracle, and whose proofs are the oracle answers. Such a specif…
A simple formalization of alpha-equivalence
Kalmer Apinis, Danel Ahman
While teaching untyped -calculus to undergraduate students, we were wondering why -equivalence is not directly inductively defined. In this paper, we demonstrate that this is…
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…
Comodule Representations of Second-Order Functionals
Danel Ahman, Andrej Bauer
We develop and investigate a general theory of representations of second-order functionals, based on a notion of a right comodule for a monad on the category of containers. We show…