@book(DBLP:books/daglib/0070479, author = {Peter B. Andrews}, year = {1986}, title = {An introduction to mathematical logic and type theory - to truth through proof}, series = {Computer science and applied mathematics}, publisher = {Academic Press}, ) @inproceedings(DBLP:conf/cade/AspertiRCT11, author = {Andrea Asperti and Wilmer Ricciotti and Claudio Sacerdoti Coen and Enrico Tassi}, year = {2011}, title = {The Matita Interactive Theorem Prover}, editor = {Bj{\o}rner, Nikolaj and Sofronie{-}Stokkermans, Viorica}, booktitle = {Automated Deduction - {CADE-23} - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {6803}, publisher = {Springer}, pages = {64--69}, url = {https://doi.org/10.1007/978-3-642-22438-6_7}, ) @inproceedings(DBLP:conf/itp/CauderlierD17, author = {Rapha{\"{e}}l Cauderlier and Catherine Dubois}, year = {2017}, title = {FoCaLiZe and Dedukti to the Rescue for Proof Interoperability}, editor = {Ayala{-}Rinc{\'{o}}n, Mauricio and Mu{\~{n}}oz, C{\'{e}}sar A.}, booktitle = {Interactive Theorem Proving - 8th International Conference, {ITP} 2017, Bras{\'{\i}}lia, Brazil, September 26-29, 2017, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {10499}, publisher = {Springer}, pages = {131--147}, url = {https://doi.org/10.1007/978-3-319-66107-0_9}, ) @inproceedings(DBLP:conf/cade/ChihaniMR13, author = {Zakaria Chihani and Dale Miller and Fabien Renaud}, year = {2013}, title = {Foundational Proof Certificates in First-Order Logic}, editor = {Maria Paola Bonacina}, booktitle = {Automated Deduction - {CADE-24} - 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {7898}, publisher = {Springer}, pages = {162--177}, url = {https://doi.org/10.1007/978-3-642-38574-2_11}, ) @inproceedings(DBLP:conf/lics/Coquand86, author = {Thierry Coquand}, year = {1986}, title = {An Analysis of Girard's Paradox}, booktitle = {Proceedings of the Symposium on Logic in Computer Science {(LICS} '86), Cambridge, Massachusetts, USA, June 16-18, 1986}, publisher = {{IEEE} Computer Society}, pages = {227--236}, ) @inproceedings(DBLP:conf/tlca/CousineauD07, author = {Denis Cousineau and Gilles Dowek}, year = {2007}, title = {Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo}, editor = {Simona Ronchi Della Rocca}, booktitle = {Typed Lambda Calculi and Applications, 8th International Conference, {TLCA} 2007, Paris, France, June 26-28, 2007, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {4583}, publisher = {Springer}, pages = {102--117}, url = {http://dx.doi.org/10.1007/978-3-540-73228-0_9}, ) @article(DBLP:journals/jacm/HarperHP93, author = {Robert Harper and Furio Honsell and Gordon D. Plotkin}, year = {1993}, title = {A Framework for Defining Logics}, journal = {J. {ACM}}, volume = {40}, number = {1}, pages = {143--184}, url = {http://doi.acm.org/10.1145/138027.138060}, ) @inproceedings(hurd2011, author = {Joe Hurd}, year = {2011}, title = {The {OpenTheory} Standard Theory Library}, editor = {Mihaela Bobaru and Klaus Havelund and Gerard J. Holzmann and Rajeev Joshi}, booktitle = {Third International Symposium on {NASA} Formal Methods ({NFM 2011})}, series = {Lecture Notes in Computer Science}, volume = {6617}, publisher = {Springer}, pages = {177--191}, url = {https://doi.org/10.1007/3-540-60275-5_76}, ) @inproceedings(DBLP:conf/itp/KellerW10, author = {Chantal Keller and Benjamin Werner}, year = {2010}, title = {Importing {HOL} Light into Coq}, editor = {Matt Kaufmann and Lawrence C. Paulson}, booktitle = {Interactive Theorem Proving, First International Conference, {ITP} 2010, Edinburgh, UK, July 11-14, 2010. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {6172}, publisher = {Springer}, pages = {307--322}, url = {https://doi.org/10.1007/978-3-642-14052-5_22}, ) @article(Pfenning:1988:HAS:960116.54010, author = {F. Pfenning and C. Elliott}, year = {1988}, title = {Higher-order Abstract Syntax}, journal = {SIGPLAN Not.}, volume = {23}, number = {7}, pages = {199--208}, url = {http://doi.acm.org/10.1145/960116.54010}, ) @inproceedings(Pientka:POPL08, author = {Brigitte Pientka}, year = {2008}, title = {A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions}, booktitle = {35th Annual {ACM} Symposium on Principles of Programming Languages (POPL'08)}, publisher = {ACM}, pages = {371--382}, url = {https://doi.org/10.1145/1328438.1328483}, ) @phdthesis(DBLP:phd/hal/Saillard15a, author = {Ronan Saillard}, year = {2015}, title = {Typechecking in the lambda-Pi-Calculus Modulo : Theory and Practice. (V{\'{e}}rification de typage pour le lambda-Pi-Calcul Modulo : th{\'{e}}orie et pratique)}, school = {Mines ParisTech, France}, url = {https://tel.archives-ouvertes.fr/tel-01299180}, ) @misc(thecoqdevelopmentteam20171133970, author = {The Coq Development Team}, year = {2017}, title = {The Coq Proof Assistant, version 8.7.1}, url = {https://doi.org/10.5281/zenodo.1133970}, ) @misc(matitaarith, author = {The Matita development team}, year = {2018}, title = {Arithmetic library}, url = {https://github.com/LPCIC/matita/tree/master/matita/matita/lib/arithmetics}, ) @misc(interop, author = {Thir\IeC{\'e}, Fran\IeC{\c c}ois}, year = {2018}, title = {Interoperability in Dedukti: From the Calculus of Inductive Constructions to an extension of HOL.}, note = {\url{http://www.lsv.fr/~fthire/research/interop/index.php}}, ) @misc(sttforall, author = {Thir\IeC{\'e}, Fran\IeC{\c c}ois}, year = {2018}, title = {Sharing a library between proof assistants: reaching out to the HOL family.}, note = {\url{http://www.lsv.fr/~fthire/research/sttforall/index.php}}, )