I am a post doctoral researcher at the University of Bologna, working with Claudio Sacerdoti Coen. I am also a concluding PhD student at LIX. My advisor is Dale Miller.
My interests are (in a somehow decreasing order of generality): proof theory, proof checking, intuitionism, proof-theoretic semantics, semi-classical logics, focusing, admissible rules of proof systems, effects in functional languages.
- IT: In Novembre e Dicembre 2021 sarò l'esercitatore per il corso 93283 - Logica per l'informatica
- I am moving to DISI, the department of Computer Science at the University of Bologna
- A new draft: Computational logic based on linear logic and fixponts, with Dale Miller: PDF
- Two applications of logic programming to Coq, 2021, with Alberto Momigliano and Dale Miller. In Ugo de'Liguoro and Stefano Berardi and Thorsten Altenkirch: 26th International Conference on Types for Proofs and Programs (TYPES 2020). DOI:10.4230/LIPIcs.TYPES.2020.10. PDF.
- A proof-theoretic approach to certifying skolemization, 2018, with Kaustuv Chaudhuri and Dale Miller. In Assia Mahboubi and Magnus O. Myreen: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, (CPP 2019), Cascais, Portugal, January 14-15, 2019, pp 78--90. DOI: 10.1145/3293880.3294094. Code
- Admissible Tools in the Kitchen of Intuitionistic Logic, 2018, with Andrea Condoluci. In Stefano Berardi and Alexandre Miquel:
Proceedings Seventh International Workshop on Classical Logic and Computation (CL&C 2018),
Oxford (UK), 7th of July 2018,
Electronic Proceedings in Theoretical Computer Science 281, pp. 1023.
- Harrop: A New Tool in the Kitchen of Intuitionistic Logic, 2018, with Andrea Condoluci. In: Proceedings of the ESSLLI 2018 Student Session.
- On Natural Deduction for Herbrand Constructive Logics II: Curry-Howard Correspondence for Markov's Principle in First-Order Logic and Arithmetic, 2016, with Federico Aschieri. In Silvia Ghilezan, Herman Geuvers and Jelena Ivetić: 22nd International Conference on Types for Proofs and Programs (TYPES 2016), 2018, Leibniz International Proceedings in Informatics (LIPIcs) 97, 4:1--4:17. arXiv.
- Linking a λProlog proof checker to the Coq kernel LFMTP 2020 (Online) June 29th, 2020 Abstract, Code, Video of the talk
- Harrop: a new tool in the Kitchen of Intuitionistic Logic ESSLLI 2018 Student Session (Sofia, BG) August 16th, 2018. Slides
- Admissible Tools in the Kitchen of Intuitionistic Logic at Classical Logic & Computation (Oxford, UK) July 7th, 2018. Slides
- Admissible Tools in the Kitchen of Intuitionistic Logic at the Parsifal team seminar, (Palaiseau, FR) May 30th, 2018. Slides
- IT: il 20 Aprile 2021 parlerò al Quarto Seminario degli ex-studenti di Matematica e Informatica dell'Università di Parma
- In the winter and spring semesters of 2020-2021 I will be teaching assistant for Logic 2 at Université Paris 1
- Until June 2020 I will be on leave at École Normale Superieure, attending the Master de Philosophie de PSL
- On January 14th I gave the talk A proof-theoretic approach to certifying skolemization at CPP 2019 in Lisbon, Portugal: Slides.
- A proof-theoretic approach to certifying skolemization, by me, Dale Miller and Kaustuv Chaudhuri has been accepted at CPP 2019 (Lisbon, Portigal). Paper.
- I will be co-chairing the ESSLLI 2019 Student Session in Riga, Latvia
- In the spring semester 18/19 I am chargé de TD for the lecture M2101 Architecture d'un systeme informatique at the IUT d'Orsay.
- In the winter semester 18/19 I am chargé de TD for the lecture M1103 (Structures de donnees et algorithmes fondamentaux) at the IUT d'Orsay.
- On Natural Deduction for Herbrand Constructive Logics II has been accepted for publication in the postproceedings of TYPES 2016
- A short version of Admissible Tools in the Kitchen of Intuitionistic Logic, by me and Andrea, has been presented at the student session of ESSLLI 2018 (Sofia, Bulgaria)
- A longer version was presented at Classical Logic & Computation (Oxford, UK)