3 citations · 3 across the 3 of their papers we have counts for
5 papers · 1 filter
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…
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…
The Next 700 Relational Program Logics
Kenji Maillard, Catalin Hritcu, Exequiel Rivas +1
We propose the first framework for defining relational program logics for arbitrary monadic effects. The framework is embedded within a relational dependent type theory and is high…
Dijkstra Monads for All
Kenji Maillard, Danel Ahman, Robert Atkey +4
This paper proposes a general semantic framework for verifying programs with arbitrary monadic side-effects using Dijkstra monads, which we define as monad-like structures indexed…
Relating Idioms, Arrows and Monads from Monoidal Adjunctions
Exequiel Rivas
We revisit once again the connection between three notions of computation: monads, arrows and idioms (also called applicative functors). We employ monoidal categories of finitary f…