nach oben

Erschienen in:

2018 | OriginalPaper | Buchkapitel

HOL Light QE

verfasst von : Jacques Carette, William M. Farmer, Patrick Laskowski

Erschienen in: Interactive Theorem Proving

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

We are interested in algorithms that manipulate mathematical expressions in mathematically meaningful ways. Expressions are syntactic, but most logics do not allow one to discuss syntax. \({\textsc {ctt}}_\mathrm{qe}\) is a version of Church’s type theory that includes quotation and evaluation operators, akin to quote and eval in the Lisp programming language. Since the \(\text {HOL}\) logic is also a version of Church’s type theory, we decided to add quotation and evaluation to \(\text {HOL Light}\) to demonstrate the implementability of \({\textsc {ctt}}_\mathrm{qe}\) and the benefits of having quotation and evaluation in a proof assistant. The resulting system is called \(\text {HOL Light QE}\). Here we document the design of \(\text {HOL Light QE}\) and the challenges that needed to be overcome. The resulting implementation is freely available.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Verified Analysis of Random Binary Tree Structures

Nächstes Kapitel Efficient Mendler-Style Lambda-Encodings in Cedille

In Lisp, the standard symbol for quasiquotation is the backquote (‘) symbol, and thus in Lisp, quasiquotation is usually called backquote.

And some personal communication with some of system authors.

Hales, T., et al.: A formal proof of the Kepler conjecture. Forum Math. Pi 5 (2017)

Allen, S.F., Constable, R.L., Howe, D.J., Aitken, W.E.: The semantics of reflected proof. In: Proceedings of the Fifth Annual Symposium on Logic in Computer Science (LICS 1990), pp. 95–105. IEEE Computer Society (1990)

Andrews, P.B.: An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, 2nd edn. Kluwer, Dordrecht (2002)

Barzilay, E.: Implementing Reflection in Nuprl. Ph.D. thesis. Cornell University (2005)

Bawden, A.: Quasiquotation in Lisp. In: Danvy, O. (ed.) Proceedings of the 1999 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pp. 4–12 (1999), Technical report BRICS-NS-99-1, University of Aarhus (1999)

Boutin, S.: Using reflection to build efficient and certified decision procedures. In: Abadi, M., Ito, T. (eds.) TACS 1997. LNCS, vol. 1281, pp. 515–529. Springer, Heidelberg (1997). https://doi.org/10.1007/BFb0014565CrossRef

Boyer, R., Moore, J.: Metafunctions: proving them correct and using them efficiently as new proof procedures. In: Boyer, R., Moore, J. (eds.) The Correctness Problem in Computer Science, pp. 103–185. Academic Press, New York (1981)

Boyer, R., Moore, J.: A Computational Logic Handbook. Academic Press, San Diego (1988)MATH

Braibant, T., Pous, D.: Tactics for reasoning modulo AC in Coq. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 167–182. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-25379-9_14CrossRef

10.

Buchberger, B., Craciun, A., Jebelean, T., Kovacs, L., Kutsia, T., Nakagawa, K., Piroi, F., Popov, N., Robu, J., Rosenkranz, M., Windsteiger, W.: Theorema: towards computer-aided mathematical theory exploration. J. Appl. Logic 4, 470–504 (2006)MathSciNetCrossRef

11.

Cappelen, H., LePore, E.: Quotation. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy, Spring 2012

12.

Carette, J., Farmer, W.M.: Formalizing mathematical knowledge as a biform theory graph: a case study. In: Geuvers, H., England, M., Hasan, O., Rabe, F., Teschke, O. (eds.) CICM 2017. LNCS (LNAI), vol. 10383, pp. 9–24. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-62075-6_2CrossRef

13.

Chaieb, A., Nipkow, T.: Proof synthesis and reflection for linear arithmetic. J. Autom. Reason. 41, 33–59 (2008)MathSciNetCrossRef

14.

Chlipala, A.: Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant. MIT Press, Cambridge (2013)MATH

15.

Christiansen, D., Brady, E.: Elaborator reflection: Extending Idris in Idris. SIGPLAN Not. 51, 284–297 (2016). https://doi.org/10.1145/3022670.2951932, http://doi.acm.org/10.1145/3022670.2951932

16.

Christiansen, D.R.: Type-directed elaboration of quasiquotations: a high-level syntax for low-level reflection. In: Proceedings of the 26nd 2014 International Symposium on Implementation and Application of Functional Languages, IFL 2014, pp. 1:1–1:9. ACM, New York (2014). https://doi.org/10.1145/2746325.2746326, http://doi.acm.org/10.1145/2746325.2746326

17.

Christiansen, D.R.: Practical Reflection and Metaprogramming for Dependent Types. Ph.D. thesis. IT University of Copenhagen (2016)

18.

Church, A.: A formulation of the simple theory of types. J. Symbolic Logic 5, 56–68 (1940)MathSciNetCrossRef

19.

Clavel, M., Meseguer, J.: Reflection in conditional rewriting logic. Theoret. Comput. Sci. 285, 245–288 (2002)MathSciNetCrossRef

20.

Constable, R.L.: Using reflection to explain and enhance type theory. In: Schwichtenberg, H. (ed.) Proof and Computation. NATO ASI Series, vol. 139, pp. 109–144. Springer, Heidelberg (1995). https://doi.org/10.1007/978-3-642-79361-5_3

21.

Constable, R.L., Allen, S.F., Bromley, H.M., Cleaveland, W.R., Cremer, J.F., Harper, R.W., Howe, D.J., Knoblock, T.B., Mendler, N.P., Panangaden, P., Sasaki, J.T., Smith, S.F.: Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Englewood Cliffs (1986)

22.

Coq Development Team: The Coq Proof Assistant Reference Manual, Version 8.5 (2016). https://coq.inria.fr/distrib/current/refman/

23.

Costantini, S.: Meta-reasoning: a survey. In: Kakas, A.C., Sadri, F. (eds.) Computational Logic: Logic Programming and Beyond. LNCS (LNAI), vol. 2408, pp. 253–288. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45632-5_11CrossRef

24.

Ebner, G., Ullrich, S., Roesch, J., Avigad, J., de Moura, L.: A metaprogramming framework for formal verification. Proc. ACM Program. Lang. 1, 34 (2017)CrossRef

25.

Farmer, W.M.: The formalization of syntax-based mathematical algorithms using quotation and evaluation. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) CICM 2013. LNCS (LNAI), vol. 7961, pp. 35–50. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39320-4_3CrossRef

26.

Farmer, W.M.: Incorporating quotation and evaluation into church’s type theory: syntax and semantics. In: Kohlhase, M., Johansson, M., Miller, B., de de Moura, L., Tompa, F. (eds.) CICM 2016. LNCS (LNAI), vol. 9791, pp. 83–98. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-42547-4_7CrossRef

27.

Farmer, W.M.: Incorporating quotation and evaluation into Church’s type theory. Inf. Comput. 260C, 9–50 (forthcoming, 2018)

28.

Giese, M., Buchberger, B.: Towards practical reflection for formal mathematics. RISC Report Series 07–05, Research Institute for Symbolic Computation (RISC). Johannes Kepler University (2007)

29.

Gonthier, G.: The four colour theorem: engineering of a formal proof. In: Kapur, D. (ed.) ASCM 2007. LNCS (LNAI), vol. 5081, pp. 333–333. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-87827-8_28CrossRef

30.

Gonthier, G., et al.: A machine-checked proof of the odd order theorem. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 163–179. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39634-2_14CrossRef

31.

Gonthier, G., Mahboubi, A.: An introduction to small scale reflection in Coq. J. Formalized Reason. 3, 95–152 (2010)MathSciNetMATH

32.

Gordon, M.J.C., Melham, T.F.: Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, New York (1993)MATH

33.

Grégoire, B., Mahboubi, A.: Proving equalities in a commutative ring done right in Coq. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 98–113. Springer, Heidelberg (2005). https://doi.org/10.1007/11541868_7CrossRefMATH

34.

Grundy, J., Melham, T., O’Leary, J.: A reflective functional language for hardware design and theorem proving. Funct. Program. 16 (2006)

35.

Harrison, J.: Metatheory and reflection in theorem proving: a survey and critique. Technical Report CRC-053. SRI Cambridge (1995). http://www.cl.cam.ac.uk/~jrh13/papers/reflect.ps.gz

36.

Harrison, J.: HOL light: an overview. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 60–66. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03359-9_4CrossRef

37.

von Henke, F.W., Pfab, S., Pfeifer, H., Rueß, H.: Case studies in meta-level theorem proving. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol. 1479, pp. 461–478. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0055152

38.

Henkin, L.: Completeness in the theory of types. J. Symbolic Logic 15, 81–91 (1950)MathSciNetCrossRef

39.

Hickey, J., Nogin, A., Constable, R.L., Aydemir, B.E., Barzilay, E., Bryukhov, Y., Eaton, R., Granicz, A., Kopylov, A., Kreitz, C., Krupski, V.N., Lorigo, L., Schmitt, S., Witty, C., Yu, X.: MetaPRL – a modular logical environment. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 287–303. Springer, Heidelberg (2003). https://doi.org/10.1007/10930755_19CrossRef

40.

Howe, D.: Reflecting the semantics of reflected proof. In: Aczel, P., Simmons, H., Wainer, S. (eds.) Proof Theory, pp. 229–250. Cambridge University Press, Cambridge (1992)

41.

Hunt Jr., W.A., Kaufmann, M., Krug, R.B., Moore, J.S., Smith, E.W.: Meta reasoning in ACL2. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 163–178. Springer, Heidelberg (2005). https://doi.org/10.1007/11541868_11CrossRef

42.

James, D.W.H., Hinze, R.: A reflection-based proof tactic for lattices in Coq. In: Horváth, Z., Zsók, V., Achten, P., Koopman, P.W.M. (eds.) Proceedings of the Tenth Symposium on Trends in Functional Programming (TFP 2009). Trends in Functional Programming, vol. 10, pp. 97–112. Intellect (2009)

43.

Kaufmann, M., Moore, J.S.: An industrial strength theorem prover for a logic based on Common Lisp. IEEE Trans. Softw. Eng. 23, 203–213 (1997)CrossRef

44.

Kavvos, G.A.: On the Semantics of Intensionality and Intensional Recursion, December 2017. http://arxiv.org/abs/1712.09302

45.

Knoblock, T.B., Constable, R.L.: Formalized metareasoning in type theory. In: Proceedings of the Symposium on Logic in Computer Science (LICS 1986), pp. 237–248. IEEE Computer Society (1986)

46.

Melham, T., Cohn, R., Childs, I.: On the semantics of ReFLect as a basis for a reflective theorem prover. Computing Research Repository (CoRR) abs/1309.5742 (2013). http://arxiv.org/abs/1309.5742

47.

Nogin, A., Kopylov, A., Yu, X., Hickey, J.: A computational approach to reflective meta-reasoning about languages with bindings. In: Pollack, R. (ed.) ACM SIGPLAN International Conference on Functional Programming, Workshop on Mechanized Reasoning about Languages with Variable Binding (MERLIN 2005), pp. 2–12. ACM (2005)

48.

Norell, U.: Dependently typed programming in Agda. In: Kennedy, A., Ahmed, A. (eds.) Proceedings of TLDI 2009, pp. 1–2. ACM (2009)

49.

Oostdijk, M., Geuvers, H.: Proof by computation in the Coq system. Theor. Comput. Sci. 272 (2002)

50.

Polonsky, A.: Axiomatizing the quote. In: Bezem, M. (ed.) Computer Science Logic (CSL 2011) – 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), vol. 12, pp. 458–469. Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

51.

Quine, W.V.O.: Mathematical Logic, Revised edn. Harvard University Press, Cambridge (2003)MATH

52.

Rabe, F.: Generic literals. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS (LNAI), vol. 9150, pp. 102–117. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-20615-8_7CrossRef

53.

Tarski, A.: The concept of truth in formalized languages. In: Corcoran, J. (ed.) Logic, Semantics, Meta-Mathematics, 2nd edn., pp. 152–278. Hackett (1983)

54.

Völker, N.: HOL2P - a system of classical higher order logic with second order polymorphism. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 334–351. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74591-4_25CrossRef

55.

van der Walt, P.: Reflection in Agda. Master’s thesis, Universiteit Utrecht (2012)

56.

van der Walt, P., Swierstra, W.: Engineering proof by reflection in agda. In: Hinze, R. (ed.) IFL 2012. LNCS, vol. 8241, pp. 157–173. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-41582-1_10CrossRef

57.

Yu, X.: Reflection and Its Application to Mechanized Metareasoning about Programming Languages. Ph.D. thesis. California Institute of Technology (2007)

Titel: HOL Light QE
verfasst von: Jacques Carette
William M. Farmer
Patrick Laskowski
Verlag: Springer International Publishing
Buch: Interactive Theorem Proving
Print ISBN: 978-3-319-94820-1

Electronic ISBN: 978-3-319-94821-8

Copyright-Jahr: 2018
DOI: https://doi.org/10.1007/978-3-319-94821-8_13

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"