Mechanized metatheory revisited. (English) Zbl 1468.68303

Summary: 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.


68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
03B35 Mechanization of proofs and logical operations
Full Text: DOI Link


[1] The Abella prover (2012). http://abella-prover.org/
[2] Abramsky, S.; Turner, DA (ed.), The lazy lambda calculus, 65-116, (1990), Reading, MA
[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) · Zbl 1385.68012
[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) · Zbl 0797.68095
[6] Andrews, PB, Resolution in type theory, J. Symb. Log., 36, 414-432, (1971) · Zbl 0231.02038
[7] Andrews, PB, Provability in elementary type theory, Zeitschrift fur Mathematische Logic und Grundlagen der Mathematik, 20, 411-418, (1974) · Zbl 0306.02017
[8] Andrews, P.B.: An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, 2nd edn. Kluwer Academic Publishers, Dordrecht (2002)
[9] Appel, AW; Felty, AP, Polymorphic lemmas and definitions in \(\lambda \)Prolog and Twelf, Theory Pract. Log. Program., 4, 1-39, (2004) · Zbl 1085.68015
[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) · Zbl 1295.68052
[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) · Zbl 1152.68516
[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] Baelde, D., Least and greatest fixed points in linear logic, ACM Trans. Comput. Log., 13, 2, (2012) · Zbl 1352.03072
[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, 1-89, (2014)
[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) · Zbl 1137.03323
[18] Barendregt, HP, Introduction to generalized type systems, J. Funct. Program., 1, 125-154, (1991) · Zbl 0931.03019
[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, 25-49, (2006) · Zbl 1095.03016
[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) · Zbl 1069.68095
[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) · Zbl 1301.68169
[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, 9:1-9:25, (2015)
[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) · Zbl 1252.68062
[26] Charguéraud, A., The locally nameless representation, J. Autom. Reason., 49, 1-46, (2011)
[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) · Zbl 1104.68370
[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) · Zbl 1323.68184
[30] Chlipala, A.: Certified Programming with Dependent Types—A Pragmatic Introduction to the Coq Proof Assistant. MIT Press, Cambridge (2013) · Zbl 1288.68001
[31] Church, A., A formulation of the simple theory of types, J. Symb. Log., 5, 56-68, (1940) · JFM 66.1192.06
[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, 36-72, (1993)
[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] Coquand, T.; Huet, G., The calculus of constructions, Inf. Comput., 76, 95-120, (1988) · Zbl 0654.03045
[36] de Bruijn, NG, Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with an application to the Church-Rosser theorem, Indag. Math., 34, 381-392, (1972) · Zbl 0253.68007
[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) · Zbl 1063.68650
[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) · Zbl 1471.68046
[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) · Zbl 0645.68097
[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) · Zbl 0708.68090
[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) · Zbl 1252.68252
[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) · Zbl 1357.68198
[46] Felty, AP; 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, 307-372, (2015) · Zbl 1357.68198
[47] Felty, AP; Momigliano, A.; Pientka, B., Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions, Math. Struct. Comput. Sci., 28, 1507-1540, (2017) · Zbl 1400.68194
[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, MJ; Pitts, AM, A new approach to abstract syntax with variable binding, Formal Aspects of Computing, 13, 341-363, (2001) · Zbl 1001.68083
[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) · Zbl 1165.68457
[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] Gacek, A.; Miller, D.; Nadathur, G., Nominal abstraction, Inf. Comput., 209, 48-73, (2011) · Zbl 1215.03049
[56] Gacek, A.; Miller, D.; Nadathur, G., A two-level logic approach to reasoning about computations, J. Autom. Reason., 49, 241-273, (2012) · Zbl 1290.68088
[57] Gentzen, G.; Szabo, ME (ed.), Investigations into logical deduction, 68-131, (1935), Amsterdam
[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) · JFM 57.0054.02
[64] Gordon, M.J.C., Melham, T.F.: Introduction to HOL—A theorem proving environment for higher order logic. Cambridge University Press, Cambridge (1993)
[65] Gordon, M.J., Milner, A.J., Wadsworth, P.: Edinburgh LCF: A Mechanised Logic of Computation, volume 78 of LNCS. Springer, Berlin (1979) · Zbl 0421.68039
[66] Gordon, M.; Plotkin, GD (ed.); Stirling, C. (ed.); Tofte, M. (ed.), From LCF to HOL: a short history, 169-186, (2000), Cambridge
[67] Hannan, J., Extended natural semantics, J. Funct. Program., 3, 123-152, (1993)
[68] Hannan, J.; Miller, D., From operational semantics to abstract machines, Math. Struct. Comput. Sci., 2, 415-459, (1992) · Zbl 0798.68099
[69] Harper, R.; Honsell, F.; Plotkin, G., A framework for defining logics, J. ACM, 40, 143-184, (1993) · Zbl 0778.03004
[70] Harrison, J.: HOL light: an overview. In: International Conference on Theorem Proving in Higher Order Logics, pp. 60-66. Springer (2009) · Zbl 1252.68255
[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, 239-285, (2001) · Zbl 0956.68095
[73] Howe, DJ, Proving congruence of bisimulation in functional programming languages, Inf. Comput., 124, 103-112, (1996) · Zbl 0853.68073
[74] Huet, G., The undecidability of unification in third order logic, Inf. Control, 22, 257-267, (1973) · Zbl 0257.02038
[75] Huet, G., A unification algorithm for typed \(\lambda \)-calculus, Theor. Comput. Sci., 1, 27-57, (1975) · Zbl 0332.02035
[76] Huet, G.; Lang, B., Proving and applying program transformations expressed with second-order patterns, Acta Inf., 11, 31-55, (1978) · Zbl 0389.68008
[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) · Zbl 0635.68007
[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) · Zbl 1079.03045
[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, 107-115, (2009)
[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) · Zbl 1102.68019
[84] MacKenzie, D.: Mechanizing Proof. MIT Press, Cambridge (2001) · Zbl 1063.68500
[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] McDowell, R.; Miller, D., Cut-elimination for a logic with definitions and induction, Theor. Comput. Sci., 232, 91-119, (2000) · Zbl 0951.03050
[90] McDowell, R.; Miller, D., Reasoning with higher-order abstract syntax in a logical framework, ACM Trans. Comput. Log., 3, 80-136, (2002) · Zbl 1365.68164
[91] Miller, D., A compact representation of proofs, Stud. Log., 46, 347-370, (1987) · Zbl 0644.03033
[92] Miller, D., A logic programming language with lambda-abstraction, function variables, and simple unification, J. Logic Comput., 1, 497-536, (1991) · Zbl 0738.68016
[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] Miller, D., Unification under a mixed prefix, J. Symb. Comput., 14, 321-358, (1992) · Zbl 0768.68067
[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) · Zbl 1095.03507
[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) · Zbl 0611.68057
[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) · Zbl 0900.68129
[100] Miller, D.; Nadathur, G.; Pfenning, F.; Scedrov, A., Uniform proofs as a foundation for logic programming, Ann. Pure Appl. Log., 51, 125-157, (1991) · Zbl 0721.03037
[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] Miller, D.; Tiu, A., A proof theory for generic judgments, ACM Trans. Comput. Log., 6, 749-783, (2005) · Zbl 1367.03059
[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) · Zbl 0683.68008
[107] Milner, R.; Parrow, J.; Walker, D., A calculus of mobile processes, Part I, Inf. Comput., 100, 1-40, (1992) · Zbl 0752.68036
[108] Milner, R.; Parrow, J.; Walker, D., A calculus of mobile processes, Part II, Inf. Comput., 100, 41-77, (1992) · Zbl 0752.68037
[109] Milner, R.; Parrow, J.; Walker, D., Modal logics for mobile processes, Theor. Comput. Sci., 114, 149-171, (1993) · Zbl 0778.68033
[110] Milner, R., Tofte, M.: Commentary on Standard ML. The MIT Press, Cambridge (1991)
[111] Mitchell, JC; Moggi, E., Kripke-style models for typed lambda calculus, Ann. Pure Appl. Log., 51, 99-124, (1991) · Zbl 0728.03011
[112] Momigliano, A., Pientka, B., Thibodeau, D.: A case-study in programming coinductive proofs: Howe’s method. Submitted (2017)
[113] Moore, JS, A mechanically verified language implementation, J. Autom. Reason., 5, 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, DS, A notation for lambda terms: a generalization of environments, Theor. Comput. Sci., 198, 49-98, (1998) · Zbl 0901.03015
[117] Nanevski, A.; Pfenning, F.; Pientka, B., Contextual model type theory, ACM Trans. Comput. Log., 9, 1-49, (2008) · Zbl 1367.03060
[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) · Zbl 1252.68262
[119] Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL—A Proof Assistant for Higher-Order Logic. Number 2283 in LNCS. Springer, Berlin (2002)
[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)
[121] Paulson, LC, Natural deduction as higher-order resolution, J. Log. Program., 3, 237-258, (1986) · Zbl 0613.68035
[122] Paulson, L.C.: Isabelle: A Generic Theorem Prover. Number 828 in LNCS. Springer Verlag, Berlin (1994)
[123] Paulson, LC, A generic tableau prover and its integration with isabelle, J. UCS, 5, 73-87, (1999) · Zbl 0961.68116
[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) · Zbl 0716.68079
[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) · Zbl 0925.03062
[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) · Zbl 1291.68366
[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) · Zbl 0963.68502
[132] Pitts, AM, Nominal logic, a first order theory of names and binding, Inf. Comput., 186, 165-193, (2003) · Zbl 1056.03014
[133] Pitts, AM, Alpha-structural recursion and induction, J. ACM, 53, 459-506, (2006) · Zbl 1326.68180
[134] Plotkin, GD, A structural approach to operational semantics, J. Log. Algebraic Program., 60-61, 17-139, (2004) · Zbl 1082.68062
[135] The POPLmark Challenge webpage. http://www.seas.upenn.edu/ plclub/poplmark/ (2015)
[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) · Zbl 1151.68551
[138] Pous, Damien: Complete lattices and upto techniques. In: Shao, Zhong (ed.) APLAS, volume 4807 of LNCS, pp. 351-366, Singapore. Springer (November 2007) · Zbl 1138.68041
[139] Pous, D.; Sangiorgi, D.; Sangiorgi, D. (ed.); Rutten, J. (ed.), Enhancements of the bisimulation proof method, 233-289, (2011), Cambridge · Zbl 1285.68111
[140] Prawitz, D., Hauptsatz for higher order logic, J. Symb. Log., 33, 452-457, (1968) · Zbl 0164.31002
[141] Qi, X., Gacek, A., Steven, H., Nadathur, G., Snow, Z.: The Teyjus system—version 2 (2015). http://teyjus.cs.umn.edu/
[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) · Zbl 0978.68045
[143] Sangiorgi, D., \(\pi \)-calculus, internal mobility and agent-passing calculi, Theor. Comput. Sci., 167, 235-274, (1996) · Zbl 0874.68103
[144] Sangiorgi, D., Walker, D.: \(\pi \)-Calculus: A Theory of Mobile Processes. Cambridge University Press, Cambridge (2001) · Zbl 0981.68116
[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) · Zbl 0924.03024
[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] Selinger, P., The lambda calculus is algebraic, J. Funct. Program., 12, 549-566, (2002) · Zbl 1040.68023
[150] Sewell, P.; Nardelli, FZ; Owens, S.; Peskine, G.; Ridge, T.; Sarkar, S.; Strniša, R., Ott: effective tool support for the working semanticist, J. Funct. Program., 20, 71-122, (2010) · Zbl 1185.68201
[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) · Zbl 1360.68601
[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)
[155] Takahashi, M., A proof of cut-elimination theorem in simple type theory, J. Math. Soc. Jpn., 19, 399-410, (1967) · Zbl 0206.27503
[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) · Zbl 1134.68451
[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, 13, (2010) · Zbl 1351.68186
[160] Tiu, A.; Momigliano, A., Cut elimination for a logic with induction and co-induction, J. Appl. Log., 10, 330-367, (2012) · Zbl 1278.03086
[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) · Zbl 1483.68050
[163] Tofte, M., Type inference for polymorphic references, Inf. Comput., 89, 1-34, (1990) · Zbl 0705.68028
[164] Urban, C., Nominal reasoning techniques in Isabelle/HOL, J. Autom. Reason., 40, 327-356, (2008) · Zbl 1140.68061
[165] Urban, C.; Cheney, J.; Berghofer, S., Mechanizing the metatheory of LF, ACM Trans. Comput. Log. (TOCL), 12, 15, (2011) · Zbl 1351.68250
[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) · Zbl 1135.68561
[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) · Zbl 1335.68036
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.