Papers & Talks

Publications, drafts and extended abstracts


POPL’24 Securing Verified IO Programs Against Unverified Code in F.
Cezar-Constantin Andrici, Ștefan Ciobâcă, Cătălin Hrițcu, Guido Martínez, Exequiel Rivas, Éric Tanter and Théo Winterhalter. The artifact received the Functional and Reusable badges.
PrePrint. Artifact


  Who Verifies the Verifiers? A Computer-Checked Implementation of the DPLL Algorithm in Dafny.
Cezar-Constantin Andrici and Ștefan Ciobâcă. In Mathematics 2022, 10(13), 2264.
HOPE’22 Verifying non-terminating programs with IO in F (Extended Abstract).
Cezar-Constantin Andrici, Théo Winterhalter, Cătălin Hrițcu and Exequiel Rivas. At the 10th ACM SIGPLAN Workshop on Higher-Order Programming with Effects.
Slides. Video. Artifact
TYPES’22 Partial Dijkstra Monads for All (Extended Abstract).
Théo Winterhalter, Cezar-Constantin Andrici, Cătălin Hrițcu, Kenji Maillard, Guido Martínez and Exequiel Rivas. At the 28th International Conference on Types for Proofs and Programs.
Slides. Artifact