Dafina Trufaș

About Me

I became interested in logic and proof assistants during the winter semester of 2021, when I attended a Lean seminar. This was also my first exposure to the functional programming paradigm.

In the summer of 2022, I completed an internship at Runtime Verification Inc., where I had my first opportunity to work as part of a proof-engineering team. During this internship, I learned the basics of theorem proving in Coq, contributed to the Correct-by-Construction Casper project, and helped improve both the project's research paper and its documentation. From July to October 2023, I completed a second internship at the same company. There, I further developed my Coq skills by contributing to the formalization of a distributed-systems framework. I also co-authored a paper demonstrating how this framework can be applied to solve an asynchronous version of the Muddy Children puzzle.

In 2024, I completed my undergraduate studies in Computer Science at the Faculty of Mathematics and Computer Science, University of Bucharest. My bachelor's thesis focused on the formalization of Intuitionistic Propositional Logic in Lean. From August 2024 to July 2025, I worked as a Research Assistant at the Institute for Logic and Data Science. 

In 2026, I graduated from the Security and Applied Logic master's programme at the University of Bucharest. My dissertation was dedicated to a new, simpler axiomatization of applicative matching logic. I am currently a Teaching Assistant at the University of Bucharest and an Associated Researcher at the Institute for Logic and Data Science (ILDS ) and at the Logic, Optimization & Security Center (LOS ).

For more details about my activity, please check my CV.

Publications

• Matching logic - a new axiomatization (with Laurențiu Leuștean), arXiv preprint arXiv:2506.13801 (2025)

• Intuitionistic Propositional Logic in Lean, Electronic Proceedings in Theoretical Computer Science (2024)

• Asynchronous Muddy Children Puzzle (work in progress) (with Ioan Teodorescu, Denisa Diaconescu, Traian Șerbănuță and Vlad Zamfir), Electronic Proceedings in Theoretical Computer Science (2023)

• Validating Labelled State Transition and Message Production Systems (with Vlad Zamfir, Mihai Calancea, Denisa Diaconescu, Wojciech Kolowski, Brandon Moore, Karl Palmskog, Traian Florin Șerbănuță, Michael Stay, Jan Tusil), arXiv preprint arXiv:2202.12662 (2022)

Talks

Contributed Conference Talks

• Working Formal Methods Symposium (FROM) 2024, Timișoara, Romania, September 16-18, 2024

• Working Formal Methods Symposium (FROM) 2023, Bucharest, Romania, September 21-22, 2023

Seminar Talks

• Intuitionistic propositional logic I,  Logic Seminar, Faculty of Mathematics and Computer Science, University of Bucharest, November 14, 2024

• Intuitionistic propositional logic II,  Logic Seminar, Faculty of Mathematics and Computer Science, University of Bucharest, November 21, 2024

Contact

You can contact me at the following email addresses: dafinatrufas@gmail.com, dafina.trufas@unibuc.ro.