References

  1. Rob Arthan: HOL Formalised: Semantics. Available at http://www.lemma-one.com/ProofPower/specs/spc002.pdf.
  2. Rob Arthan (2014): HOL Constant Definition Done Right. In: Interactive Theorem Proving. Springer International Publishing, pp. 531–536, doi:10.1007/978-3-319-08970-6_34.
  3. William M. Farmer: A General Method for Safely Overwriting Theories in Mechanized Mathematics Systems. Available at http://imps.mcmaster.ca/doc/overwriting-theories.pdf.
  4. Arve Gengelbach & Tjark Weber (2017): Model-Theoretic Conservative Extension for Definitional Theories. In: Sandra Alves & Renata Wasserman: 12th Workshop on Logical and Semantic Frameworks, with Applications, LSFA 2017, Brasília, Brazil, September 23-24, 2017, Electronic Notes in Theoretical Computer Science 338. Elsevier, pp. 133–145, doi:10.1016/j.entcs.2018.10.009.
  5. Arve Gengelbach & Tjark Weber (2020): Proof-theoretic Conservativity for HOL with Ad-hoc Overloading. In: Violet Ka I Pun, Volker Stolz & Adenilso da Silva Simão: Theoretical Aspects of Computing - ICTAC 2020 - 17th International Colloquium, Macau, China, November 30 - December 4, 2020, Proceedings, Lecture Notes in Computer Science 12545. Springer, pp. 23–42, doi:10.1007/978-3-030-64276-1_2.
  6. Adam Grabowski, Artur Kornilowicz & Adam Naumowicz (2010): Mizar in a Nutshell. J. Formalized Reasoning 3(2), pp. 153–245, doi:10.6092/issn.1972-5787/1980.
  7. Florian Haftmann & Makarius Wenzel (2006): Constructive Type Classes in Isabelle. 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. 160–174, doi:10.1007/978-3-540-74464-1_11.
  8. Ramana Kumar, Rob Arthan, Magnus O. Myreen & Scott Owens (2014): HOL with Definitions: Semantics, Soundness, and a Verified Implementation. In: Interactive Theorem Proving. Springer, Cham, pp. 308–324, doi:10.1007/978-3-319-08970-6_20.
  9. Ramana Kumar, Rob Arthan, Magnus O. Myreen & Scott Owens (2016): Self-Formalisation of Higher-Order Logic - Semantics, Soundness, and a Verified Implementation. J. Autom. Reasoning 56(3), doi:10.1007/s10817-015-9357-x.
  10. Ondrej Kuncar (2015): Correctness of Isabelle's Cyclicity Checker: Implementability of Overloading in Proof Assistants. In: Xavier Leroy & Alwen Tiu: Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015. ACM, pp. 85–94, doi:10.1145/2676724.2693175.
  11. Ondrej Kuncar & Andrei Popescu (2018): Safety and conservativity of definitions in HOL and Isabelle/HOL. PACMPL 2(POPL), pp. 24:1–24:26, doi:10.1145/3158112.
  12. Ondrej Kuncar & Andrei Popescu (2019): A Consistent Foundation for Isabelle/HOL. J. Autom. Reasoning 62(4), pp. 531–555, doi:10.1007/s10817-018-9454-8.
  13. Ondřej Kunčar & Andrei Popescu (2017): Comprehending Isabelle/HOL's Consistency. In: Hongseok Yang: Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Lecture Notes in Computer Science 10201. Springer, pp. 724–749, doi:10.1007/978-3-662-54434-1_27.
  14. Michael Norrish & Konrad Slind (2014): The HOL System LOGIC. Available at http://downloads.sourceforge.net/project/hol/hol/kananaskis-10/kananaskis-10-logic.pdf.
  15. Steven Obua (2006): Checking Conservativity of Overloaded Definitions in Higher-Order Logic. In: Frank Pfenning: Term Rewriting and Applications, 17th International Conference, RTA 2006, Seattle, WA, USA, August 12-14, 2006, Proceedings, Lecture Notes in Computer Science 4098. Springer, pp. 212–226, doi:10.1007/11805618_16.
  16. Andrew M. Pitts (1993): The HOL Logic. In: M.J.C. Gordon & Tom Melham: Introduction to HOL: A Theorem-Proving Environment for Higher-Order Logic. Cambridge University Press, pp. 191–232.
  17. Johannes Åman Pohjola & Arve Gengelbach (2020): A Mechanised Semantics for HOL with Ad-hoc Overloading. In: Elvira Albert & Laura Kovács: LPAR23. LPAR-23: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, EPiC Series in Computing 73. EasyChair, pp. 498–515, doi:10.29007/413d. Available at https://easychair.org/publications/paper/9Hcd.
  18. Piotr Rudnicki (1992): An Overview of the Mizar Project. In: Bengt Nordström, Kent Petersson & Gordon Plotkin: Proceedings of the 1992 Workshop on Types for Proofs and Programs, pp. 311–332. Available at http://mizar.org/project/MizarOverview.pdf.
  19. Joseph R. Shoenfield (1967): Mathematical Logic. A.K. Peters, Natick, Mass.
  20. Markus Wenzel (1997): Type Classes and Overloading in Higher-Order Logic. In: Elsa L. Gunter & Amy P. Felty: Theorem Proving in Higher Order Logics, 10th International Conference, TPHOLs'97, Murray Hill, NJ, USA, August 19-22, 1997, Proceedings, Lecture Notes in Computer Science 1275. Springer, pp. 307–322, doi:10.1007/BFb0028402.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org