Papers & Talks

Misquoted No More: Securely Extracting F* programs with IOCezar-Constantin Andrici, Abigail Pribisova, Danel Ahman, Cătălin Hrițcu, Exequiel Rivas, and Théo Winterhalter. DOIArtifactThe artifact received the Functional and Reusable badges.

SecRef*: Securely Sharing Mutable References between Verified and Unverified Code in F*Cezar-Constantin Andrici, Danel Ahman, Cătălin Hrițcu, Ruxandra Icleanu, Guido Martínez, Exequiel Rivas, and Théo Winterhalter. DOISlidesArtifactThe artifact received the Functional and Reusable badges.

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. DOIVideoPoP Up VideoArtifactThe artifact received the Functional and Reusable badges.

A Verified Implementation of the DPLL Algorithm in DafnyCezar-Constantin Andrici and Ștefan Ciobâcă. Artifact

Verifying non-terminating programs with IO in F* (Extended Abstract)Cezar-Constantin Andrici, Théo Winterhalter, Cătălin Hrițcu and Exequiel Rivas. SlidesVideoArtifact

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. Artifact

Verifying the DPLL Algorithm in DafnyCezar-Constantin Andrici and Ștefan Ciobâcă.

Secure extraction of verified effectful F* programs to MLAt Aarhus University, April 13, 2026. Slides

Gradual Enforcement of IO Trace Properties at Student Research CompetitionAt the 25th ACM SIGPLAN International Conference on Functional Programming (ICFP), August 2020. Video🏆 First place winner of ICFP SRC 2020, graduate section.

Verification of IO programs in F*At the Faculty of Computer Science, UAIC, January 2020.

Proofs are Programs — Teaching Assistant, RUB, Bochum (Fall)

Functional Programming — Teaching Assistant, RUB, Bochum (Summer)

Logics in Computer Science — Teaching Assistant, UAIC, Iași (Fall)

CPP’26, ICFP’25, POPL’24, SP’21

Committee member at POPL’26, POPL’23

POPL’24, POPL’23, ICFP’22, PLDI’20, POPL’20, ETAPS’19, FROM’18