Proofs, upside down: a functional correspondence between natural deduction and the sequent calculus M Puech Asian Symposium on Programming Languages and Systems, 365-380, 2013 | 6 | 2013 |
Typeful normalization by evaluation O Danvy, C Keller, M Puech 20th International Conference on Types for Proofs and Programs, TYPES 2014, 2014 | 5 | 2014 |
Certificates for Incremental Type Checking M Puech Università di Bologna, Université Paris Diderot, 2013 | 2 | 2013 |
Reconnaissance automatique de structures mathématiques dans l’assistant de preuve Coq M Puech Master’s thesis, Université Paris Diderot - Paris 7, 2008 | 2 | 2008 |
A functional correspondence between natural deduction and sequent calculus M Puech TYPES, 2013 | 1 | 2013 |
Typeful Continuations M Puech JFLA 2017-28ème Journées Francophones des Langages Applicatifs, 1-14, 2017 | | 2017 |
Safe Incremental Type Checking M Puech, Y Régis-Gianas TLDI 2012-Seventh ACM SIGPLAN Workshop on Types in Language Design and …, 2012 | | 2012 |
Towards typed repositories of proofs M Puech, Y Régis-Gianas Mathematically Intelligent Proof Search-MIPS 2010, 2010 | | 2010 |
HAL Id: inria-00525874 M Puech, Y Régis-Gianas | | |
Certifying, incremental type checking M Puech, Y Régis-Gianas | | |