Matteo Manighetti

About me

I am a Research Engineer at IRIF, the research center in theoretical computer science of the Paris Cité University. You can contact me at surname at irif.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 have been at Inria Saclay, in the Toccata team. Before that, 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 (To appear in Fundamenta Informaticae. Last update Nov. 2024)

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)