Matteo Manighetti
About me
I am a Research Engineer (French: Ingénieur de Recherche) at Inria
Saclay, in the Toccata team.
You can contact me at name.surname at inria.fr.
My interests are (in a somehow decreasing order of generality): proof
theory, proof checking and proof assistants, intuitionism, proof-theoretic
semantics, semi-classical logics, focusing, admissible rules of proof
systems, effects in functional languages.
Previously, I was a research assistant at the University of Bologna, working
with Claudio Sacerdoti Coen. I obtained my PhD in Computer Science in 2023
from the Institut Polytechnique de Paris, where my advisor has been Dale Miller.
Drafts and preprints
- Peano Arithmetic and μMALL, with Dale Miller: arXiv (2023)
Papers
- 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.
HAL.
- 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.
Talks
- Applications of focusing to the proof theory of arithmetic Mathematical Logic Webinar, Universidade de Lisboa (Online) February 1st, 2021 Slides
- 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
News Archive
- 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
- 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)
Me on Mastodon