@mastersthesis(Aguirre16,
 author       = {Alejandro Aguirre},
 year         = {2016},
 title        = {{Towards a provably correct encoding from F* to SMT}},
 url          = {https://prosecco.gforge.inria.fr/personal/hritcu/students/alejandro/report.pdf},
)
@inproceedings(armandkeller11,
 author       = {Micha{\"e}l Armand and Germain Faure and Benjamin Gr{\'e}goire and Chantal Keller and Laurent Thery and Benjamin Werner},
 year         = {2011},
 title        = {A Modular Integration of {SAT/SMT} Solvers to {Coq} through Proof Witnesses},
 booktitle    = {First International Conference on Certified Programs and Proofs},
 doi          = {10.1007/978-3-642-25379-9\_12},
)
@inproceedings(lambdapi16,
 author       = {Ali Assaf and Guillaume Burel and Raphal Cauderlier and David Delahaye and Gilles Dowek and Catherine Dubois and Fr{\'e}d{\'e}ric Gilbert and Pierre Halmagrand and Olivier Hermant and Ronan Saillard},
 year         = {2016},
 title        = {Expressing theories in the {$\lambda$$\Pi$}-calculus modulo theory and in the {Dedukti} system},
 booktitle    = {22nd International Conference on Types for Proofs and Programs},
 url          = {https://hal-mines-paristech.archives-ouvertes.fr/hal-01441751},
)
@article(barendregt2002autarkic,
 author       = {Henk Barendregt and Erik Barendsen},
 year         = {2002},
 title        = {Autarkic computations in formal proofs},
 journal      = {Journal of Automated Reasoning},
 doi          = {10.1023/A:1015761529444},
)
@inproceedings(CAC,
 author       = {Fr{\'{e}}d{\'{e}}ric Blanqui},
 year         = {2003},
 title        = {Inductive Types in the Calculus of Algebraic Constructions},
 series       = {Lecture Notes in Computer Science},
 doi          = {10.1007/3-540-44904-3\_4},
)
@article(bobot14sttt,
 author       = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and Claude March\'e and Andrei Paskevich},
 year         = {2015},
 title        = {Let's Verify This with {Why3}},
 journal      = {International Journal on Software Tools for Technology Transfer (STTT)},
 doi          = {10.1007/s10009-014-0314-5},
)
@misc(bobotPaskevich2011poly,
 author       = {Fran\c{c}ois Bobot and Andrei Paskevich},
 year         = {2011},
 title        = {{Expressing Polymorphic Types in a Many-Sorted Language}},
 doi          = {10.1007/978-3-642-24364-6\_7},
)
@inproceedings(DBLP:conf/itp/BohmeW10,
 author       = {Sascha B{\"{o}}hme and Tjark Weber},
 year         = {2010},
 title        = {Fast {LCF}-Style Proof Reconstruction for {Z3}},
 booktitle    = {Interactive Theorem Proving},
 doi          = {10.1007/978-3-642-14052-5\_14},
)
@inproceedings(DBLP:journals/corr/CauderlierH15,
 author       = {Rapha{\"{e}}l Cauderlier and Pierre Halmagrand},
 year         = {2015},
 title        = {Checking {Zenon} Modulo Proofs in {Dedukti}},
 booktitle    = {Proof eXchange for Theorem Proving},
 doi          = {10.4204/EPTCS.186.7},
)
@inproceedings(chihani2013checking,
 author       = {Zakaria Chihani and Dale Miller and Fabien Renaud},
 year         = {2013},
 title        = {Checking Foundational Proof Certificates for First-Order Logic (Extended Abstract)},
 booktitle    = {PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving},
 doi          = {10.29007/7gnr},
)
@inproceedings(contejean08types,
 author       = {\'Evelyne Contejean},
 year         = {2008},
 title        = {{Coccinelle, a Coq library for rewriting}},
 booktitle    = {Types},
)
@inproceedings(PTS,
 author       = {Denis Cousineau and Gilles Dowek},
 year         = {2007},
 title        = {Embedding Pure Type Systems in the lambda-Pi-calculus modulo},
 booktitle    = {Typed lambda calculi and applications},
 doi          = {10.1007/978-3-540-73228-0\_9},
)
@inproceedings(delahaye2000tactic,
 author       = {David Delahaye},
 year         = {2000},
 title        = {A tactic language for the system Coq},
 booktitle    = {International Conference on Logic for Programming Artificial Intelligence and Reasoning},
 doi          = {10.1007/3-540-44404-1\_7},
)
@phdthesis(filliatre99preuve,
 author       = {Jean-Christophe Filli\^atre},
 year         = {1999},
 title        = {{Preuve de programmes imp\'eratifs en th\'eorie des types}},
 url          = {http://www.lri.fr/~filliatr/ftp/publis/these.ps.gz},
)
@misc(bugdestcase,
 author       = {Quentin Garchery},
 year         = {2021},
 title        = {{destruct/case transformations incorrectly handle polymorphic formulas}},
 howpublished = {\url{https://gitlab.inria.fr/why3/why3/-/issues/525/}},
)
@misc(p_shadow,
 author       = {Quentin Garchery},
 year         = {2021},
 title        = {{Performance slowdown with variable shadowing}},
 howpublished = {\url{https://github.com/Deducteam/lambdapi/issues/565}},
)
@misc(p_context,
 author       = {Quentin Garchery},
 year         = {2021},
 title        = {{Performance with growing context}},
 howpublished = {\url{https://github.com/Deducteam/lambdapi/issues/579}},
)
@misc(p_var_hyp,
 author       = {Quentin Garchery},
 year         = {2021},
 title        = {{Performances with both new variables and hypotheses in context}},
 howpublished = {\url{https://github.com/Deducteam/lambdapi/issues/595}},
)
@misc(p_linear,
 author       = {Quentin Garchery},
 year         = {2021},
 title        = {{Performances with linear propositional problem}},
 howpublished = {\url{https://github.com/Deducteam/lambdapi/issues/649}},
)
@misc(p_nested,
 author       = {Quentin Garchery},
 year         = {2021},
 title        = {{Performances with nested applications in context}},
 howpublished = {\url{https://github.com/Deducteam/lambdapi/issues/584}},
)
@misc(branchpxtp,
 author       = {Quentin Garchery},
 year         = {2021},
 title        = {{Why3 cert\_pxtp branch}},
 url          = {https://gitlab.inria.fr/why3/why3/-/blob/cert_pxtp/README_PXTP.md},
)
@inproceedings(garchery:hal-02384946,
 author       = {Quentin Garchery and Chantal Keller and Claude March{\'e} and Andrei Paskevich},
 year         = {2020},
 title        = {{Des transformations logiques passent leur certicat}},
 booktitle    = {{JFLA 2020 - Journ{\'e}es Francophones des Langages Applicatifs}},
 address      = {Gruissan, France},
 url          = {https://hal.inria.fr/hal-02384946},
)
@phdthesis(greenaway15phd,
 author       = {David Greenaway},
 year         = {2015},
 title        = {Automated proof-producing abstraction of C code},
 school       = {CSE, UNSW},
 url          = {http://unsworks.unsw.edu.au/fapi/datastream/unsworks:13743/SOURCE02?view=true},
)
@inproceedings(greenaway14pldi,
 author       = {David Greenaway and Japheth Lim and June Andronick and Gerwin Klein},
 year         = {2014},
 title        = {Don't Sweat the Small Stuff: Formal Verification of {C} Code Without the Pain},
 booktitle    = {ACM SIGPLAN Conference on Programming Language Design and Implementation},
 doi          = {10.1145/2594291.2594296},
)
@inproceedings(DBLP:conf/flops/GregoireTW06,
 author       = {Benjamin Gr{\'{e}}goire and Laurent Th{\'{e}}ry and Benjamin Werner},
 year         = {2006},
 title        = {A Computational Approach to {Pocklington} Certificates in Type Theory},
 booktitle    = {Functional and Logic Programming},
 doi          = {10.1007/11737414\_8},
)
@inproceedings(DBLP:conf/fsttcs/Huet87,
 author       = {G{\'{e}}rard P. Huet},
 year         = {1987},
 title        = {The Calculus of Constructions: State of the Art},
 booktitle    = {Foundations of Software Technology and Theoretical Computer Science},
 doi          = {10.1007/3-540-18625-5\_61},
)
@inproceedings(iris17,
 author       = {Robbert Krebbers and Ralf Jung and Ale\v{s} Bizjak and Jacques-Henri Jourdan and Derek Dreyer and Lars Birkedal},
 year         = {2017},
 title        = {The Essence of Higher-Order Concurrent Separation Logic},
 booktitle    = {26th European Symposium on Programming Languages and Systems},
 doi          = {10.1007/978-3-662-54434-1\_26},
)
@phdthesis(Lescuyer11,
 author       = {St{\'{e}}phane Lescuyer},
 year         = {2011},
 title        = {Formalizing and Implementing a Reflexive Tactic for Automated Deduction in Coq. (Formalisation et developpement d'une tactique reflexive pour la demonstration automatique en coq)},
 school       = {University of Paris-Sud, Orsay, France},
 url          = {https://tel.archives-ouvertes.fr/tel-00713668},
)
@article(milner1978theory,
 author       = {Robin Milner},
 year         = {1978},
 title        = {A theory of type polymorphism in programming},
 journal      = {Journal of computer and system sciences},
 doi          = {10.1016/0022-0000(78)90014-4},
)
@inproceedings(PfenningP89,
 author       = {Frank Pfenning and Paulin{-}Mohring, Christine},
 year         = {1989},
 title        = {Inductively Defined Types in the Calculus of Constructions},
 series       = {Lecture Notes in Computer Science},
 doi          = {10.1007/BFb0040259},
)
@inproceedings(DBLP:conf/popl/SwamyHKRDFBFSKZ16,
 author       = {Nikhil Swamy and Catalin Hritcu and Chantal Keller and Aseem Rastogi and Delignat{-}Lavaud, Antoine and Simon Forest and Karthikeyan Bhargavan and C{\'{e}}dric Fournet and Pierre{-}Yves Strub and Markulf Kohlweiss and Jean Karim Zinzindohoue and Santiago Zanella B{\'{e}}guelin},
 year         = {2016},
 title        = {Dependent types and multi-monadic effects in {F*}},
 booktitle    = {Principles of Programming Languages},
 doi          = {10.1145/2837614.2837655},
)