A proof-theoretic approach to certifying skolemization K Chaudhuri, M Manighetti, D Miller
Proceedings of the 8th ACM SIGPLAN International Conference on Certified …, 2019
4 2019 Admissible tools in the kitchen of intuitionistic logic A Condoluci, M Manighetti
arXiv preprint arXiv:1810.07372, 2018
4 2018 Two applications of logic programming to Coq M Manighetti, D Miller, A Momigliano
26th International Conference on Types for Proofs and Programs (TYPES 2020), 2021
3 2021 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
3 2016 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 Expressiveness of extensions of MALL with fixpoints and induction M Manighetti
2019 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
