References

  1. Haniel Barbosa, Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli & Clark W. Barrett (2019): Extending SMT Solvers to Higher-Order Logic. In: Pascal Fontaine: Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings, Lecture Notes in Computer Science 11716. Springer, pp. 35–54, doi:10.1007/978-3-030-29436-6_3.
  2. Frédéric Besson (2006): Fast Reflexive Arithmetic Tactics the Linear Case and Beyond. In: Thorsten Altenkirch & Conor McBride: Types for Proofs and Programs, International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers, Lecture Notes in Computer Science 4502. Springer, pp. 48–62, doi:10.1007/978-3-540-74464-1_4.
  3. Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu & Nicholas Smallbone (2016): Encoding Monomorphic and Polymorphic Types. Log. Methods Comput. Sci. 12(4), doi:10.2168/LMCS-12(4:13)2016.
  4. François Bobot & Andrey Paskevich (2011): Expressing Polymorphic Types in a Many-Sorted Language. In: Cesare Tinelli & Viorica Sofronie-Stokkermans: Frontiers of Combining Systems, 8th International Symposium, FroCoS 2011, Saarbrücken, Germany, October 5-7, 2011. Proceedings, Lecture Notes in Computer Science 6989. Springer, pp. 87–102, doi:10.1007/978-3-642-24364-6_7.
  5. Sascha Böhme & Tjark Weber (2010): Fast LCF-Style Proof Reconstruction for Z3. In: Matt Kaufmann & Lawrence C. Paulson: Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, Lecture Notes in Computer Science 6172. Springer, pp. 179–194, doi:10.1007/978-3-642-14052-5_14.
  6. Adam Chlipala (2013): Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant. MIT Press. Available at http://mitpress.mit.edu/books/certified-programming-dependent-types.
  7. Lukasz Czajka & Cezary Kaliszyk (2018): Hammer for Coq: Automation for Dependent Type Theory. J. Autom. Reason. 61(1-4), pp. 423–453, doi:10.1007/s10817-018-9458-4.
  8. David Delahaye (2000): A Tactic Language for the System Coq. In: Michel Parigot & Andrei Voronkov: Logic for Programming and Automated Reasoning, 7th International Conference, LPAR 2000, Reunion Island, France, November 11-12, 2000, Proceedings, Lecture Notes in Computer Science 1955. Springer, pp. 85–95, doi:10.1007/3-540-44404-1_7.
  9. Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds & Clark W. Barrett (2017): SMTCoq: A Plug-In for Integrating SMT Solvers into Coq. In: Rupak Majumdar & Viktor Kuncak: Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II, Lecture Notes in Computer Science 10427. Springer, pp. 126–133, doi:10.1007/978-3-319-63390-9_7.
  10. Jean-Christophe Filliâtre & Andrei Paskevich (2013): Why3 - Where Programs Meet Provers. In: Matthias Felleisen & Philippa Gardner: Programming Languages and Systems - 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings, Lecture Notes in Computer Science 7792. Springer, pp. 125–128, doi:10.1007/978-3-642-37036-6_8.
  11. Benjamin Grégoire & Assia Mahboubi (2005): Proving Equalities in a Commutative Ring Done Right in Coq. In: Joe Hurd & Thomas F. Melham: Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings, Lecture Notes in Computer Science 3603. Springer, pp. 98–113, doi:10.1007/11541868_7.
  12. J. Hurd (2005): System Description: The Metis Proof Tactic. Empirically Successful Automated Reasoning in Higher-Order Logic (ESHOL), pp. 103–104.
  13. 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.
  14. Lawrence C. Paulson (1999): A Generic Tableau Prover and its Integration with Isabelle. J. Univers. Comput. Sci. 5(3), pp. 73–87, doi:10.3217/jucs-005-03-0073.
  15. Lawrence C. Paulson & Jasmin Christian Blanchette (2010): Three years of experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers. In: Geoff Sutcliffe, Stephan Schulz & Eugenia Ternovska: The 8th International Workshop on the Implementation of Logics, IWIL 2010, Yogyakarta, Indonesia, October 9, 2011, EPiC Series in Computing 2. EasyChair, pp. 1–11. Available at https://easychair.org/publications/paper/wV.
  16. Pierre-Marie Pédrot (2019): Ltac2: tactical warfare. CoqPL 2019.
  17. Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau & Théo Winterhalter (2020): The MetaCoq Project. J. Autom. Reason. 64(5), pp. 947–999, doi:10.1007/s10817-019-09540-0.
  18. Enrico Tassi (2019): Deriving Proved Equality Tests in Coq-Elpi: Stronger Induction Principles for Containers in Coq. In: John Harrison, John O'Leary & Andrew Tolmach: 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA, LIPIcs 141. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 29:1–29:18, doi:10.4230/LIPIcs.ITP.2019.29.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org