5 citations · 13 across the 7 of their papers we have counts for
9 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…
Formalizing a classification theorem for low-dimensional solvable Lie algebras in Lean
Viviana del Barco, Gustavo Infanti, Exequiel Rivas +1
We present a formalization, in the theorem prover Lean, of the classification of solvable Lie algebras of dimension at most three over arbitrary fields. Lie algebras are algebraic…
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…
Securing Verified IO Programs Against Unverified Code in F*
Cezar-Constantin Andrici, Stefan Ciobaca, Catalin Hritcu +4
We introduce SCIO*, a formally secure compilation framework for statically verified partial programs performing input-output (IO). The source language is an F* subset in which a ve…
Interaction laws of monads and comonads
Shin-ya Katsumata, Exequiel Rivas, Tarmo Uustalu
We introduce and study functor-functor and monad-comonad interaction laws as mathematical objects to describe interaction of effectful computations with behaviors of effect-perform…
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…
Notions of Computation as Monoids
Exequiel Rivas, Mauro Jaskelioff
There are different notions of computation, the most popular being monads, applicative functors, and arrows. In this article we show that these three notions can be seen as monoids…