I pursued my PhD at IT University of Copenhagen with main supervisor Marco Carbone and co-supervisor Jesper Bengtson. During my PhD I mechanised subject reduction and communication safety, based on their formulation in Honda et al. [1]. This was carried out in the Coq Proof Assistant. The thesis can be found here and links for developments are provided below.
Open to network
I am interested in formal methods and their use in practice. Having spent now some years in academia, I now seek a research position in industry where formal methods are used in practice. Feel free to get in contact on dawit.tirore@gmail.com
Publications
- A sound and Complete Projection for Global Types publised in the Interactive Theorem Proving conference in 2023 pdf code
Theses
- MSc thesis: A Propositional Calculus for Contract Specification pdf code
- PhD thesis: A Mechanisation of Multiparty Session Types pdf
Projects in Coq
-
Subject reduction for multiparty session types (paper under review) code
-
Computational interpretation of regular expression containment proofs, based on the work of Henglein and Nielsen [2] (report under development) code
Projects in Isabelle/HOL
References
[1]: Kohei Honda, Nobuko Yoshida, Marco Carbone; Multiparty Asynchronous Session Types.
[2]: Fritz Henglein, Lasse Nielsen; Regular expression containment: coinductive axiomatization and computational interpretation