A proof-theoretic approach to certifying skolemization K Chaudhuri, M Manighetti, D Miller
Proceedings of the 8th ACM SIGPLAN International Conference on Certified …, 2019
5 2019 Admissible tools in the kitchen of intuitionistic logic A Condoluci, M Manighetti
arXiv preprint arXiv:1810.07372, 2018
4 2018 On Natural Deduction for Herbrand Constructive Logics II: Curry-Howard Correspondence for Markov's Principle in First-Order Logic and Arithmetic F Aschieri, M Manighetti
arXiv preprint arXiv:1612.05457, 2016
4 2016 Two applications of logic programming to coq M Manighetti, D Miller, A Momigliano
LEIBNIZ INTERNATIONAL PROCEEDINGS IN INFORMATICS 188, 10: 1-10: 19, 2021
3 2021 Computational Interpretations of Markov's principle M Manighetti
Technische Universität Wien, 2016
3 2016 Developing proof theory for proof exchange M Manighetti
Institut Polytechnique de Paris, 2023
2 2023 FPC-Coq: Using Elpi to elaborate external proof evidence into Coq proofs R Blanco, M Manighetti, D Miller
Inria Saclay, 2020
2 2020 Computational logic based on linear logic and fixed points M Manighetti, D Miller
1 2022 Peano Arithmetic and M Manighetti, D Miller
arXiv preprint arXiv:2312.13634, 2023
2023 LIPIcs, Volume 188, TYPES 2020, Complete Volume}} U de'Liguoro, S Berardi, T Altenkirch, A Abel, R Affeldt, D Nowak, ...
26th International Conference on Types for Proofs and Programs (TYPES 2020 …, 2020
2020 Expressiveness of extensions of MALL with fixpoints and induction M Manighetti
2019 LIPIcs, Volume 97, TYPES'16, Complete Volume}} S Ghilezan, H Geuvers, J Ivetic, D Miller, S Ronchi Della Rocca, R Adams, ...
22nd International Conference on Types for Proofs and Programs (TYPES 2016 …, 2016
2016 Peano Arithmetic and µMALL (an abstract) M Manighetti, D Miller
Linking a λProlog proof checker to the Coq kernel An extended abstract R Blanco, M Manighetti, D Miller
