I am a PhD student at LIX, funded by INRIA Saclay. 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.
- 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
- 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)
Laboratoire d'Informatique (LIX)
91128 Palaiseau Cedex - France
Email : (First letter of my name)(first 7 letters of my surname) @ lix.polytechnique.fr
Tous les documents fournis le sont sous la responsabilité de leurs auteurs, et ne représentent pas nécessairement les positions officielles de l'École polytechnique. Les informations données le sont de bonne foi, mais leur véracité ne saurait être garantie.