References

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