Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Journal of Automated Reasoning
Published in: Journal of Automated Reasoning 3/2019

04-10-2018

Mechanized Metatheory Revisited

Author: Dale Miller

Published in: Journal of Automated Reasoning | Issue 3/2019

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

When proof assistants and theorem provers implement the metatheory of logical systems, they must deal with a range of syntactic expressions (e.g., types, formulas, and proofs) that involve variable bindings. Since most mature proof assistants do not have built-in methods to treat bindings, they have been extended with various packages and libraries that allow them to encode such syntax using, for example, de Bruijn numerals. We put forward the argument that bindings are such an intimate aspect of the structure of expressions that they should be accounted for directly in the underlying programming language support for proof assistants and not via packages and libraries. We present an approach to designing programming languages and proof assistants that directly supports bindings in syntax. The roots of this approach can be found in the mobility of binders between term-level bindings, formula-level bindings (quantifiers), and proof-level bindings (eigenvariables). In particular, the combination of Church’s approach to terms and formulas (found in his Simple Theory of Types) and Gentzen’s approach to proofs (found in his sequent calculus) yields a framework for the interaction of bindings with a full range of logical connectives and quantifiers. We will also illustrate how that framework provides a direct and semantically clean treatment of computation and reasoning with syntax containing bindings. Some implemented systems, which support this intimate and built-in treatment of bindings, will be briefly described.
previous article Reinterpreting Dependency Schemes: Soundness Meets Incompleteness in DQBF
next article Classification of Finite Fields with Applications

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now
Footnotes
1
The reader who is not familiar with the term HOAS can safely skip to the last paragraph of this section.
 
Literature
1.
2.
Abramsky, S.: The lazy lambda calculus. In: Turner, D.A. (ed.) Research Topics in Functional Programming, pp. 65–116. Addison-Welsey, Reading, MA (1990)
3.
Accattoli, B.: Proof pearl: Abella formalization of lambda calculus cube property. In: Hawblitzel, C., Miller, D. (eds.) Second International Conference on Certified Programs and Proofs, volume 7679 of LNCS, pp. 173–187. Springer (2012)
4.
Ahn, K.Y., Horne, R., Tiu, A.: A Characterisation of Open Bisimilarity using an Intuitionistic Modal Logic. In: Meyer, R., Nestmann, U. (eds.) 28th International Conference on Concurrency Theory (CONCUR 2017), volume 85 of Leibniz International Proceedings in Informatics (LIPIcs), pp. 7:1–7:17, Dagstuhl, Germany, 2017. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik (2017)
5.
Altenkirch, T.: A formalization of the strong normalization proof for system F in LEGO. In: Typed Lambda Calculi and Applications (TLCA), volume 664, pp. 13–28 (1993)
6.
7.
Andrews, P.B.: Provability in elementary type theory. Zeitschrift fur Mathematische Logic und Grundlagen der Mathematik 20, 411–418 (1974)MathSciNetMATHCrossRef
8.
Andrews, P.B.: An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, 2nd edn. Kluwer Academic Publishers, Dordrecht (2002)MATHCrossRef
9.
Appel, A.W., Felty, A.P.: Polymorphic lemmas and definitions in \(\lambda \)Prolog and Twelf. Theory Pract. Log. Program. 4(1–2), 1–39 (2004)MathSciNetMATHCrossRef
10.
Aydemir, B., Charguéraud, A., Pierce, B.C., Pollack, R., Weirich, S.: Engineering formal metatheory. In: 35th ACM Symposium on Principles of Programming Languages, pp. 3–15. ACM (2008)
11.
Aydemir, B., Zdancewic, S.A., Weirich, S.: Abstracting syntax. Technical Report MS-CIS-09-06, University of Pennsylvania (2009)
12.
Aydemir, B.E., Bohannon, A., Fairbairn, M., Foster, J.N., Pierce, B.C., Sewell, P., Vytiniotis, D., Washburn, G., Weirich, S., Zdancewic, S.: Mechanized metatheory for the masses: The POPLmark challenge. In: Theorem Proving in Higher Order Logics: 18th International Conference, number 3603 in LNCS, pp. 50–65. Springer (2005)
13.
Baelde, D.: On the expressivity of minimal generic quantification. In: Abel, A., Urban, C. (eds.) International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2008), number 228 in ENTCS, pp. 3–19 (2008)
14.
15.
Baelde, D., Chaudhuri, K., Gacek, A., Miller, D., Nadathur, G., Tiu, A., Wang, Y.: Abella: a system for reasoning about relational specifications. J. Formaliz. Reason. 7(2), 1–89 (2014)MathSciNetMATH
16.
Baelde, D., Gacek, A., Miller, D., Nadathur, G., Tiu, A.: The Bedwyr system for model checking over syntactic expressions. In: Pfenning, F. (ed.) 21th Conf. on Automated Deduction (CADE), number 4603 in LNAI, pp. 391–397, New York. Springer (2007)
17.
Baelde, D., Miller, D.: Least and greatest fixed points in linear logic. In: Dershowitz, N., Voronkov, A. (eds.) International Conference on Logic for Programming and Automated Reasoning (LPAR), volume 4790 of LNCS, pp. 92–106 (2007)
18.
19.
Benzmüller, C., Miller, D.: Automation of higher-order logic. In: Siekmann, J. (ed.) Computational Logic, volume 9 of Handbook of the History of Logic, pp. 215–254. North Holland (2014)
20.
Berger, U., Berghofer, S., Letouzey, P., Schwichtenberg, H.: Program extraction from normalization proofs. Stud. Log. 82(1), 25–49 (2006)MathSciNetMATHCrossRef
21.
Bertot, Y., Castéran, P.: Interactive theorem proving and program development. Coq’Art: the calculus of inductive constructions. Texts in theoretical computer science. Springer, Berlin (2004)MATHCrossRef
22.
Bonchi, F., Pous, D.: Checking NFA equivalence with bisimulations up to congruence. In: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 457–468. ACM (2013)
23.
Borgstrom, J., Gutkovas, R., Rodhe, I., Victor, B.: The psi-calculi workbench: a generic tool for applied process calculi. ACM Trans. Embed. Comput. Syst. 14(1), 9:1–9:25 (2015)CrossRef
24.
Borras, P., Clément, D., Despeyroux, Th., Incerpi, J., Kahn, G., Lang, B., Pascual, V.: Centaur: the system. In: Third Annual Symposium on Software Development Environments (SDE3), pp. 14–24, Boston (1988)
25.
Bove, A., Dybjer, P., Norell, U.: A brief overview of Agda—a functional language with dependent types. In: TPHOLs, volume 5674, pp. 73–78. Springer (2009)
26.
27.
Chaudhuri, K., Cimini, M., Miller, D.: A lightweight formalization of the metatheory of bisimulation-up-to. In: Leroy, X., Tiu, A. (eds.) Proceedings of the 4th ACM-SIGPLAN Conference on Certified Programs and Proofs, pp. 157–166, Mumbai, India, (2015). ACM
28.
Cheney, J., Urban, C.: Alpha-Prolog: a logic programming language with names, binding, and alpha-equivalence. In: Demoen, B., Lifschitz, V. (eds.) Logic Programming, 20th International Conference, volume 3132 of LNCS, pp. 269–283. Springer (2004)
29.
Chlipala, A.: Parametric higher-order abstract syntax for mechanized semantics. In: Hook, J., Thiemann, P. (eds.) Proceeding of the 13th ACM SIGPLAN International Conference on Functional Programming, ICFP 2008, Victoria, BC, Canada, September 20-28, 2008, pp. 143–156. ACM (2008)
30.
Chlipala, A.: Certified Programming with Dependent Types—A Pragmatic Introduction to the Coq Proof Assistant. MIT Press, Cambridge (2013)MATHCrossRef
31.
32.
Cleaveland, R., Parrow, J., Steffen, B.: The concurrency workbench: a semantics-based tool for the verification of concurrent systems. ACM Trans. Program. Lang. Syst. (TOPLAS) 15(1), 36–72 (1993)CrossRef
33.
Clément, D., Despeyroux, J., Despeyroux, T., Hascoët, L., Kahn, G.: Natural semantics on the computer. Research Report 416, INRIA, Rocquencourt, France (1985)
34.
Constable, R.L.: Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Upper Saddle River (1986)
35.
36.
de Bruijn, N.G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with an application to the Church–Rosser theorem. Indag. Math. 34(5), 381–392 (1972)MathSciNetMATHCrossRef
37.
Despeyroux, J., Felty, A., Hirschowitz, A.: Higher-order abstract syntax in Coq. In: Second International Conference on Typed Lambda Calculi and Applications, pp. 124–138 (1995)
38.
Donzeau-Gouge, V., Huet, G., Kahn, G., Lang, B.: Programming environments based on structured editors: The MENTOR experience. Technical report, Inria (1980)
39.
Dunchev, C., Coen, C.S., Tassi, E.: Implementing HOL in an higher order logic programming language. In: Dowek, G., Licata, D. R., Alves, S. (eds.) Proceedings of the Eleventh Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2016, Porto, Portugal, June 23, 2016, pp. 4:1–4:10. ACM (2016)
40.
Dunchev, C., Guidi, F., Coen, C. S., Tassi, E.: ELPI: fast, embeddable, \(\lambda \)Prolog interpreter. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning—20th International Conference, LPAR-20 2015, Suva, Fiji, November 24–28, 2015, Proceedings, volume 9450 of LNCS, pp. 460–468. Springer (2015)
41.
Eriksson, L.-H.: Pi: an interactive derivation editor for the calculus of partial inductive definitions. In: Bundy, A. (ed.) Proceedings of the Twelfth International Conference on Automated Deduction, volume 814 of LNAI, pp. 821–825. Springer (1994)
42.
Felty, A., Miller, D.: Specifying theorem provers in a higher-order logic programming language. In: Ninth International Conference on Automated Deduction, number 310 in LNCS, pp. 61–80, Argonne, IL. Springer (1988)
43.
Felty, A., Miller, D.: Encoding a dependent-type \(\lambda \)-calculus in a logic programming language. In: Stickel, M. (ed.) Proceedings of the 1990 Conference on Automated Deduction, volume 449 of LNAI, pp. 221–235. Springer (1990)
44.
Felty, A., Momigliano, A.: Hybrid: a definitional two-level approach to reasoning with higher-order abstract syntax. J. Autom. Reason. 48, 43–105 (2012)MATHCrossRef
45.
Felty, A. P., Momigliano, A., Pientka, B.: The next 700 challenge problems for reasoning with higher-order abstract syntax representations: Part 1–A common infrastructure for benchmarks. Technical report, Arxiv (2015)
46.
Felty, A.P., Momigliano, A., Pientka, B.: The next 700 challenge problems for reasoning with higher-order abstract syntax representations: Part 2-A survey. J. Autom. Reason. 55(4), 307–372 (2015)MathSciNetMATHCrossRef
47.
Felty, A.P., Momigliano, A., Pientka, B.: Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions. Math. Struct. Comput. Sci. 28, 1507–1540 (2017)MathSciNetMATHCrossRef
48.
Fiore, M.P., Plotkin, G.D., Turi, D.: Abstract syntax and variable binding. In: 14th Symposium on Logic in Computer Science, pp. 193–202. IEEE Computer Society Press (1999)
49.
Gabbay, M.J., Pitts, A.M.: A new approach to abstract syntax involving binders. In: 14th Symposium on Logic in Computer Science, pp. 214–224. IEEE Computer Society Press (1999)
50.
Gabbay, M.J., Pitts, A.M.: A new approach to abstract syntax with variable binding. Formal Aspects of Computing 13, 341–363 (2001)MATHCrossRef
51.
Gacek, Andrew: The Abella interactive theorem prover (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) Fourth International Joint Conference on Automated Reasoning, volume 5195 of LNCS, pp. 154–161. Springer (2008)
52.
Gacek, A.: A Framework for Specifying, Prototyping, and Reasoning about Computational Systems. Ph.D. thesis, University of Minnesota (2009)
53.
Gacek, A.: Relating nominal and higher-order abstract syntax specifications. In: Proceedings of the 2010 Symposium on Principles and Practice of Declarative Programming, pp. 177–186. ACM (2010)
54.
Gacek, A., Miller, D., Nadathur, G.: Combining generic judgments with recursive definitions. In: Pfenning, F. (ed.) 23th Symposium on Logic in Computer Science, pp. 33–44. IEEE Computer Society Press (2008)
55.
56.
Gacek, A., Miller, D., Nadathur, G.: A two-level logic approach to reasoning about computations. J. Autom. Reason. 49(2), 241–273 (2012)MathSciNetMATHCrossRef
57.
Gentzen, G.: Investigations into logical deduction. In: Szabo, M.E. (ed.) The Collected Papers of Gerhard Gentzen, pp. 68–131. North-Holland, Amsterdam (1935)
58.
Gentzen, Gerhard: New version of the consistency proof for elementary number theory. In: Szabo, M.E. (ed.) Collected Papers of Gerhard Gentzen, pp. 252–286. North-Holland, Amsterdam, 1938. Originally published (1938)
59.
Gérard, U., Miller, D.: Separating functional computation from relations. In: Goranko, V., Dam, M. (eds.) 26th EACSL Annual Conference on Computer Science Logic (CSL 2017), volume 82 of LIPIcs, pp. 23:1–23:17 (2017)
60.
Gérard, U., Miller, D.: Functional programming with \(\lambda \)-tree syntax: a progress report. In: 13th international Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, Oxford, United Kingdom (2018)
61.
Girard, J.-Y.: Une extension de l’interpretation de Gödel à l’analyse, et son application à l’élimination des coupures dans l’analyse et la théorie des types. In: Fenstad, J.E. (ed.) 2nd Scandinavian Logic Symposium, pp. 63–92. North-Holland, Amsterdam (1971)
62.
Girard, J.-Y.: A fixpoint theorem in linear logic. An email posting to the mailing list linear@cs.stanford.edu, (1992)
63.
Gödel, K.: Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. Monatshefte der Mathematischen Physik 38, 173–198 (1931). English Version in [167]MATHCrossRef
64.
Gordon, M.J.C., Melham, T.F.: Introduction to HOL—A theorem proving environment for higher order logic. Cambridge University Press, Cambridge (1993)MATH
65.
Gordon, M.J., Milner, A.J., Wadsworth, P.: Edinburgh LCF: A Mechanised Logic of Computation, volume 78 of LNCS. Springer, Berlin (1979)MATHCrossRef
66.
Gordon, M.: From LCF to HOL: a short history. In: Plotkin, G.D., Stirling, C., Tofte, M. (eds.) Proof, Language, and Interaction: Essays in Honour of Robin Milner, pp. 169–186. MIT Press, Cambridge (2000)MATH
67.
68.
69.
70.
Harrison, J.: HOL light: an overview. In: International Conference on Theorem Proving in Higher Order Logics, pp. 60–66. Springer (2009)
71.
Hofmann, M.: Semantical analysis of higher-order abstract syntax. In: 14th Symposium on Logic in Computer Science, pp. 204–213. IEEE Computer Society Press (1999)
72.
Honsell, F., Miculan, M., Scagnetto, I.: \(\pi \)-calculus in (co)inductive type theories. Theor. Comput. Sci. 2(253), 239–285 (2001)MATHCrossRef
73.
74.
75.
Huet, G.: A unification algorithm for typed \(\lambda \)-calculus. Theor. Comput. Sci. 1, 27–57 (1975)MATHCrossRef
76.
Huet, G., Lang, B.: Proving and applying program transformations expressed with second-order patterns. Acta Inf. 11, 31–55 (1978)MathSciNetMATHCrossRef
77.
Kahn, G.: Natural semantics. In: Brandenburg, F.-J., Vidal-Naquet, G., Wirsing, M. (eds.) Proceedings of the Symposium on Theoretical Aspects of Computer Science, volume 247 of LNCS, pp. 22–39. Springer (1987)
78.
Kaiser, J., Pientka, B., Smolka, G.: Relating system F and \(\lambda \)2: A case study in Coq, Abella and Beluga. In: Miller, D. (ed.) FSCD 2017—1st International Conference on Formal Structures for Computation and Deduction, pp. 21:1–21:19, Oxford, UK (2017)
79.
Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: Formal verification of an OS kernel. In: Proceedings of the 22nd Symposium on Operating Systems Principles (22nd SOSP’09), Operating Systems Review (OSR), pp. 207–220, Big Sky, MT. ACM SIGOPS (2009)
80.
Kohlenbach, U., Oliva, P.: Proof mining: a systematic way of analysing proofs in mathematics. Proc. Steklov Inst. Math. 242, 136–164 (2003)MATH
81.
Lee, P., Pfenning, F., Rollins, G., Scherlis, W.: The Ergo Support System: An integrated set of tools for prototyping integrated environments. In: Henderson, P. (ed.) Proceedings of the ACM SIGSOFT/SIGPLAN Software Engineering Symposium on Practical Software Development Environments, pp. 25–34. ACM Press (1988)
82.
Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009)CrossRef
83.
Liang, C., Nadathur, G., Qi, X.: Choices in representing and reduction strategies for lambda terms in intensional contexts. J. Autom. Reason. 33, 89–132 (2005)MATHCrossRef
84.
85.
Maksimović, P., Schmitt, A.: HOCore in coq. In: Interactive Theorem Proving—6th International Conference, ITP 2015, Nanjing, China, August 24–27, 2015, Proceedings, number 9236 in LNCS, pp. 278–293. Springer (2015)
86.
Martin-Löf, Per: Intuitionistic Type Theory. Studies in Proof Theory Lecture Notes. Bibliopolis, Napoli (1984)
87.
McDowell, Raymond: Reasoning in a Logic with Definitions and Induction. Ph.D. thesis, University of Pennsylvania (1997)
88.
McDowell, R., Miller, D.: A logic for reasoning with higher-order abstract syntax. In: Glynn, W. (ed.) 12th Symposium on Logic in Computer Science, pp. 434–445, Warsaw, Poland. IEEE Computer Society Press (1997)
89.
90.
McDowell, R., Miller, D.: Reasoning with higher-order abstract syntax in a logical framework. ACM Trans. Comput. Log. 3(1), 80–136 (2002)MathSciNetMATHCrossRef
91.
92.
Miller, D.: A logic programming language with lambda-abstraction, function variables, and simple unification. J. Logic Comput. 1(4), 497–536 (1991)MathSciNetMATHCrossRef
93.
Miller, D.: Abstract syntax and logic programming. In: Logic Programming: Proceedings of the First Russian Conference on Logic Programming, 14-18 September 1990, number 592 in LNAI, pp. 322–337. Springer (1992)
94.
95.
Miller, D.: Bindings, mobility of bindings, and the \(\nabla \)-quantifier. In: Marcinkowski, J., Tarlecki, A. (eds.) 18th International Conference on Computer Science Logic (CSL) 2004, volume 3210 of LNCS, pp. 24 (2004)
96.
Miller, D.: Finding unity in computational logic. In: Proceedings of the 2010 ACM-BCS Visions of Computer Science Conference, ACM-BCS ’10, pp. 3:1–3:13. British Computer Society (2010)
97.
Miller, D., Nadathur, G.: Higher-order logic programming. In: Shapiro, E. (ed.) Proceedings of the Third International Logic Programming Conference, pp. 448–462, London (1986)
98.
Miller, D., Nadathur, G.: A logic programming approach to manipulating formulas and programs. In: Haridi, S. (ed.) IEEE Symposium on Logic Programming, pp. 379–388, San Francisco (1987)
99.
Miller, D., Nadathur, G.: Programming with Higher-Order Logic. Cambridge University Press, Cambridge (2012)MATHCrossRef
100.
Miller, D., Nadathur, G., Pfenning, F., Scedrov, A.: Uniform proofs as a foundation for logic programming. Ann. Pure Appl. Log. 51(1–2), 125–157 (1991)MathSciNetMATHCrossRef
101.
Miller, D., Nadathur, G., Scedrov, A.: Hereditary Harrop formulas and uniform proof systems. In: Gries, D. (ed.) 2nd Symposium on Logic in Computer Science, pp. 98–105, Ithaca, NY (1987)
102.
Miller, D., Palamidessi, C.: Foundational aspects of syntax. ACM Computing Surveys (1999)
103.
Miller, D., Tiu, A.: A proof theory for generic judgments: An extended abstract. In: Kolaitis, P.: (ed.) 18th Symposium on Logic in Computer Science, pp. 118–127. IEEE (2003)
104.
105.
Miller, D. A., Cohen, E. L., Andrews, P. B.: A look at TPS. In: Loveland, D. W. (ed.) Sixth Conference on Automated Deduction, volume 138 of LNCS, pp. 50–69, New York, Springer (1982)
106.
Milner, R.: Communication and Concurrency. Prentice-Hall International, Upper Saddle River (1989)MATH
107.
Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, Part I. Inf. Comput. 100(1), 1–40 (1992)MATHCrossRef
108.
Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, Part II. Inf. Comput. 100(1), 41–77 (1992)MATHCrossRef
109.
110.
Milner, R., Tofte, M.: Commentary on Standard ML. The MIT Press, Cambridge (1991)
111.
112.
Momigliano, A., Pientka, B., Thibodeau, D.: A case-study in programming coinductive proofs: Howe’s method. Submitted (2017)
113.
Moore, J.S.: A mechanically verified language implementation. J. Autom. Reason. 5(4), 461–492 (1989)
114.
Nadathur, G., Miller, D.: An overview of \(\lambda \) prolog. In: Fifth International Logic Programming Conference, pp. 810–827, Seattle. MIT Press (1988)
115.
Nadathur, G., Mitchell, D. J.: System description: Teyjus—a compiler and abstract machine based implementation of \(\lambda \)Prolog. In: Ganzinger, H. (ed.) 16th Conference on Automated Deduction (CADE), number 1632 in LNAI, pp. 287–291, Trento. Springer (1999)
116.
Nadathur, G., Wilson, D.S.: A notation for lambda terms: a generalization of environments. Theor. Comput. Sci. 198(1–2), 49–98 (1998)MathSciNetMATHCrossRef
117.
118.
Naumowicz, A., Korniłowicz, A.: A brief overview of Mizar. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) Theorem Proving in Higher Order Logics, volume 5674 of LNCS, pp. 67–72 (2009)
119.
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL—A Proof Assistant for Higher-Order Logic. Number 2283 in LNCS. Springer, Berlin (2002)MATH
120.
Nordstrom, B., Petersson, K., Smith, J.M.: Programming in Martin–Löf’s Type Theory: An Introduction. International Series of Monographs on Computer Science. Clarendon, Oxford (1990)MATH
121.
122.
Paulson, L.C.: Isabelle: A Generic Theorem Prover. Number 828 in LNCS. Springer Verlag, Berlin (1994)CrossRef
123.
Paulson, L.C.: A generic tableau prover and its integration with isabelle. J. UCS 5(3), 73–87 (1999)MathSciNetMATH
124.
Perlis, A.J.: Epigrams on programming. ACM SIGPLAN Notices, pp. 7–13 (1982)
125.
Pfenning, F.: Elf: a language for logic definition and verified metaprogramming. In: 4th Symposium on Logic in Computer Science, pp. 313–321, Monterey, CA (1989)
126.
Pfenning, F., Elliott, C.: Higher-order abstract syntax. In: Proceedings of the ACM-SIGPLAN Conference on Programming Language Design and Implementation, pp. 199–208. ACM Press (1988)
127.
Pfenning, F., Rohwedder, E.: Implementing the meta-theory of deductive systems. In: Proceedings of the 1992 Conference on Automated Deduction, number 607 in LNCS, pp. 537–551. Springer (1992)
128.
Pfenning, F., Schürmann, C.: System description: Twelf—A meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) 16th Conference on Automated Deduction (CADE), number 1632 in LNAI, pp. 202–206, Trento. Springer (1999)
129.
Pientka, B., Dunfield, J.: Beluga: a framework for programming and reasoning with deductive systems (system description). In: Giesl, J., Hähnle, R. (eds.) Fifth International Joint Conference on Automated Reasoning, number 6173 in LNCS, pp. 15–21 (2010)
130.
Pierce, B.C., de Amorim, A.A., Casinghino, C., Gaboardi, M., Greenberg, M., Hricu, C., Sjöberg, V., Tolmach, A., Yorgey, B.: Programming Language Foundations, volume 2 of Software Foundations. Online (2010)
131.
Pitts, A.M., Gabbay, M.J.: A Metalanguage for Programming with Bound Names Modulo Renaming. In: Backhouse, R., Oliveira, J.N. (eds.) Mathematics of Program Construction. 5th International Conference, MPC2000, Ponte de Lima, Portugal, July 2000. Proceedings, volume 1837 of LNCS, pp. 230–255. Springer, Heidelberg (2000)
132.
133.
134.
Plotkin, G.D.: A structural approach to operational semantics. J. Log. Algebraic Program. 60–61, 17–139 (2004)MathSciNetMATH
135.
136.
Pottier, F.: Static name control for FreshML. In: 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), pp. 356–365. IEEE (2007)
137.
Pous, D.: Weak bisimulation upto elaboration. In: Baier, C., Hermanns, H. (eds.) CONCUR, volume 4137 of LNCS, pp. 390–405. Springer (2006)
138.
Pous, Damien: Complete lattices and upto techniques. In: Shao, Zhong (ed.) APLAS, volume 4807 of LNCS, pp. 351–366, Singapore. Springer (November 2007)
139.
Pous, D., Sangiorgi, D.: Enhancements of the bisimulation proof method. In: Sangiorgi, D., Rutten, J. (eds.) Advanced Topics in Bisimulation and Coinduction, pp. 233–289. Cambridge University Press, Cambridge (2011)MATHCrossRef
140.
141.
142.
Röckl, C., Hirschkoff, D., Berghofer, S.: Higher-order abstract syntax with induction in Isabelle/HOL: Formalizing the pi-calculus and mechanizing the theory of contexts. In: Honsell, F., Miculan, M. (eds.) Proceedings of the FOSSACS’01, volume 2030 of LNCS, pp. 364–378. Springer (2001)
143.
144.
Sangiorgi, D., Walker, D.: \(\pi \)-Calculus: A Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)MATH
145.
Schroeder-Heister, P.: Rules of definitional reflection. In: Vardi, M. (ed.) 8th Symposium on Logic in Computer Science, pp. 222–232. IEEE Computer Society Press, IEEE (1993)
146.
Schürmann, C., Pfenning, F.: Automated theorem proving in a simple meta-logic for LF. In: Kirchner, C., Kirchner, H. (eds.) 15th Conference on Automated Deduction (CADE), volume 1421 of Lecture Notes in Computer Science, pp. 286–300. Springer (1998)
147.
Schwichtenberg, H.: MINLOG reference manual. LMU München, Mathematisches Institut, Theresienstraße, 39 (2011)
148.
Scott, D.: Outline of a mathematical theory of computation. In: Proceedings, Fourth Annual Princeton Conference on Information Sciences and Systems, pp. 169–176. Princeton University, 1970. Also, Programming Research Group Technical Monograph PRG–2, Oxford University (1970)
149.
150.
Sewell, P., Nardelli, F.Z., Owens, S., Peskine, G., Ridge, T., Sarkar, S., Strniša, R.: Ott: effective tool support for the working semanticist. J. Funct. Program. 20(01), 71–122 (2010)MATHCrossRef
151.
Snow, Z., Baelde, D., Nadathur, G.: A meta-programming approach to realizing dependently typed logic programming. In: Kutsia, T., Schreiner, W., Fernández, M. (eds.) ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP), pp. 187–198 (2010)
152.
Southern, M., Chaudhuri, K.: A two-level logic approach to reasoning about typed specification languages. In: Raman, V., Suresh, S.P. (eds.) 34th International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), volume 29 of Leibniz International Proceedings in Informatics (LIPIcs), pp. 557–569, New Delhi, India, December 2014. Schloss Dagstuhl–Leibniz-Zentrum für Informatik (2014)
153.
Southern, M., Nadathur, G.: A \(\lambda \)Prolog based animation of Twelf specifications. The International Colloquium on Implementation of Constraint and Logic Programming Systems (CICLOPS) (2014)
154.
Stump, A.: Verified Functional Programming in Agda. Morgan & Claypool, San Rafael (2016)CrossRef
155.
156.
Tiu, A.: A Logical Framework for Reasoning about Logical Specifications. Ph.D. thesis, Pennsylvania State University (2004)
157.
Tiu, A.: Model checking for \(\pi \)-calculus using proof search. In: Abadi, M., de Alfaro, L. (eds.) Proceedings of CONCUR’05, volume 3653 of LNCS, pp. 36–50. Springer (2005)
158.
Tiu, A.: A logic for reasoning about generic judgments. In: Momigliano, A., Pientka, B. (eds.) International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP’06), volume 173 of ENTCS, pp. 3–18 (2006)
159.
Tiu, A., Miller, D.: Proof search specifications of bisimulation and modal logics for the \(\pi \)-calculus. ACM Trans. Comput. Log. 11(2), 13 (2010)MathSciNetMATHCrossRef
160.
161.
Tiu, A., Nadathur, G., Miller, D.: Mixing finite success and finite failure in an automated prover. In: Empirically Successful Automated Reasoning in Higher-Order Logics (ESHOL’05), pp. 79–98 (2005)
162.
Tiu, A., Nguyen, N., Horne, R.: SPEC: An equivalence checker for security protocols. In: Igarashi, A. (ed.) Programming Languages and Systems: 14th Asian Symposium, APLAS 2016, Hanoi, Vietnam, November 21 - 23, 2016, Proceedings, pp. 87–95. Springer International Publishing (2016)
163.
164.
Urban, C.: Nominal reasoning techniques in Isabelle/HOL. J. Autom. Reason. 40(4), 327–356 (2008)MATHCrossRef
165.
Urban, C., Cheney, J., Berghofer, S.: Mechanizing the metatheory of LF. ACM Trans. Comput. Log. (TOCL) 12(2), 15 (2011)MathSciNetMATH
166.
Urban, C., Tasson, C.: Nominal techniques in Isabelle/HOL. In: Nieuwenhuis, R. (ed.) 20th Conference on Automated Deduction (CADE), volume 3632 of LNCS, pp. 38–53. Springer (2005)
167.
van Heijenoort, J.: From Frege to Gödel: A Source Book in Mathematics, 1879-1931. Source books in the history of the sciences series. Harvard University Press, Cambridge, MA, 3rd printing, 1997 edition (1967)
168.
VanInwegen, M.: The Machine-Assisted Proof of Programming Language Properties. Ph.D. thesis, University of Pennsylvania (1996)
169.
Victor, B., Moller, F.: The mobility workbencha tool for the \(\pi \)-calculus. In: Computer Aided Verification, pp. 428–440. Springer (1994)
170.
Wang, Y.: A Higher-Order Abstract Syntax Approach to the Verified Compilation of Functional Programs. Ph.D. thesis, University of Minnesota (2016)
171.
Wang, Y., Chaudhuri, K., Gacek, A., Nadathur, G.: Reasoning about higher-order relational specifications. In: Schrijvers, T. (ed.) Proceedings of the 15th International Symposium on Princples and Practice of Declarative Programming (PPDP), pp. 157–168, Madrid, Spain (2013)
172.
Wang, Y., Nadathur, G.: A higher-order abstract syntax approach to verified transformations on functional programs. In: Thiemann, P. (ed.) Programming Languages and Systems—25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2–8, 2016, Proceedings, volume 9632 of Lecture Notes in Computer Science, pp. 752–779. Springer (2016)
Metadata
Title
Mechanized Metatheory Revisited
Author
Dale Miller
Publication date
04-10-2018
Publisher
Springer Netherlands
Published in
Journal of Automated Reasoning / Issue 3/2019
Print ISSN: 0168-7433
Electronic ISSN: 1573-0670
DOI
https://doi.org/10.1007/s10817-018-9483-3

Other articles of this Issue 3/2019

Journal of Automated Reasoning 3/2019 Go to the issue

OriginalPaper

Reinterpreting Dependency Schemes: Soundness Meets Incompleteness in DQBF

OriginalPaper

Wombit: A Portfolio Bit-Vector Solver Using Word-Level Propagation

OriginalPaper

Classification of Finite Fields with Applications

OriginalPaper

Formalization of Geometric Algebra in HOL Light

OriginalPaper

Formally Verifying the Solution to the Boolean Pythagorean Triples Problem

OriginalPaper

Semantics of Mizar as an Isabelle Object Logic

Premium Partner

    Image Credits