Top

Journal of Automated Reasoning

Published in:

16-04-2019

A Formalized General Theory of Syntax with Bindings: Extended Version

Authors: Lorenzo Gheri, Andrei Popescu

Published in: Journal of Automated Reasoning | Issue 4/2020

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

search-config

AI-assisted search

Off

Abstract

We present the formalization of a theory of syntax with bindings that has been developed and refined over the last decade to support several large formalization efforts. Terms are defined for an arbitrary number of constructors of varying numbers of inputs, quotiented to alpha-equivalence and sorted according to a binding signature. The theory contains a rich collection of properties of the standard operators on terms, including substitution, swapping and freshness—namely, there are lemmas showing how each of the operators interacts with all the others and with the syntactic constructors. The theory also features induction and recursion principles and support for semantic interpretation, all tailored for smooth interaction with the bindings and the standard operators.

next article Homogeneous Length Functions on Groups: Intertwined Computer and Human Proofs

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

On the other hand, some authors have shown that, using a clever bookkeeping of the free and bound variables, several constructions, including parallel substitution, can work smoothly on quasiterms [87, 103].

This is a contrived example, where no “real” recursion occurs—but it illustrates the point.

Note that requiring \(|{\textsf {vars}}{\textsf {Of}}\;p| < |\mathbf{var}|\) is the same as requiring that \({\textsf {vars}}{\textsf {Of}}\;p\) be finite.

The formalization work mentioned in this paragraph is mostly unpublished, although aspects concerning the involved recursive definitions are discussed in [89, 91]. Our recent draft [45] gives a detailed account of (an updated version of) the Church-Rosser and Standardization developments.

This work was the first entry in the (today very prolific) IsaFoL project [57].

Here, by “code generator” we refer to a tool for producing code (definitions, theorems and proofs) in a proof assistant, not in a programming language.

However, any generic development, even in dependent type theory, seems to require some code generation in order to offer truly usable instances—as explained, e.g., by the authors of GMeta [64, §3.1].

The difficulties of achieving this with nominal logic recursion are analyzed in [84, §6.3].

Abel, A., Momigliano, A., Pientka, B.: POPLMark Reloaded. In: LFMTP (2017)

Allais, G., Atkey, R., Chapman, J., McBride, C., McKinna, J.: A type and scope safe universe of syntaxes with binding: their semantics and proofs. In: PACMPL 2(ICFP), pp. 90:1–90:30 (2018)

Allais, G., Chapman, J., McBride, C., McKinna, J.: Type-and-scope safe programs and their proofs. In: CPP, pp. 195–207 (2017)

Altenkirch, T., Ghani, N., Hancock, P., McBride, C., Morris, P.: Indexed containers. J. Funct. Program. 25, (2015)

Altenkirch, T., Reus, B.: Monadic presentations of lambda terms using generalized inductive types. In: CSL, pp. 453–468 (1999)

Aydemir, B., Weirich, S.: LNgen: Tool support for locally nameless representations. Tech. rep., UPenn (2010)

Aydemir, B.E., Bohannon, A., Weirich, S.: Nominal reasoning techniques in Coq (extended abstract). Electr. Notes Theor. Comput. Sci. 174(5), 69–77 (2007)CrossRef

Aydemir, B.E., Charguéraud, A., Pierce, B.C., Pollack, R., Weirich, S.: Engineering formal metatheory. In: POPL, pp. 3–15 (2008)

Baelde, D., Chaudhuri, K., Gacek, A., Miller, D., Nadathur, G., Tiu, A., Wang, Y.: Abella: a system for reasoning about relational specifications. J. Formalized Reason. 7(2), 1–89 (2014)MathSciNetMATH

10.

Barendregt, H.P.: The Lambda Calculus. North-Holland, Amsterdam (1984)MATH

11.

Bauer, A., Gross, J., Lumsdaine, P.L., Shulman, M., Sozeau, M., Spitters, B.: The HoTT library: a formalization of homotopy type theory in Coq. In: CPP, pp. 164–172 (2017)

12.

Bengtson, J., Parrow, J., Weber, T.: Psi-calculi in Isabelle. J. Autom. Reason. 56(1), 1–47 (2016)MathSciNetCrossRef

13.

Berghofer, S., Urban, C.: A head-to-head comparison of De Bruijn indices and names. Electr. Notes Theor. Comput. Sci. 174(5), 53–67 (2007)CrossRef

14.

Berghofer, S., Wenzel, M.: Inductive datatypes in HOL—Lessons learned in formal-logic engineering. In: TPHOLs, pp. 19–36 (1999)

15.

Bird, R.S., Paterson, R.: De Bruijn notation as a nested datatype. J. Funct. Program 9(1), 77–91 (1999)MathSciNetCrossRef

16.

Blanchette, J.C., Böhme, S., Popescu, A., Smallbone, N.: Encoding monomorphic and polymorphic types. In: TACAS, pp. 493–507 (2013)

17.

Blanchette, J.C., Böhme, S., Popescu, A., Smallbone, N.: Encoding monomorphic and polymorphic types. Log. Methods Comput. Sci. https://doi.org/10.2168/LMCS-2014-1018

18.

Blanchette, J.C., Bouzy, A., Lochbihler, A., Popescu, A., Traytel, D.: Friends with benefits–implementing corecursion in foundational proof assistants. In: ESOP, pp. 111–140 (2017)

19.

Blanchette, J.C., Gheri, L., Popescu, A., Traytel, D.: Bindings as bounded natural functors. In: PACMPL 3(POPL), pp. 22:1–22:34 (2019)

20.

Blanchette, J.C., Hölzl, J., Lochbihler, A., Panny, L., Popescu, A., Traytel, D.: Truly modular (co)datatypes for Isabelle/HOL. In: ITP, pp. 93–110 (2014)

21.

Blanchette, J.C., Meier, F., Popescu, A., Traytel, D.: Foundational nonuniform (co)datatypes for higher-order logic. In: LICS, pp. 1–12 (2017)

22.

Blanchette, J.C., Popescu, A.: Mechanizing the metatheory of Sledgehammer. In: FroCoS, pp. 245–260 (2013)

23.

Blanchette, J.C., Popescu, A., Traytel, D.: Cardinals in Isabelle/HOL. In: ITP, pp. 111–127 (2014)

24.

Blanchette, J.C., Popescu, A., Traytel, D.: Unified classical logic completeness–a coinductive pearl. IJCAR 2014, 46–60 (2014)MathSciNetMATH

25.

Blanchette, J.C., Popescu, A., Traytel, D.: Foundational extensible corecursion: a proof assistant perspective. In: ICFP, pp. 192–204 (2015)

26.

Blanchette, J.C., Popescu, A., Traytel, D.: Soundness and completeness proofs by coinductive methods. J. Autom. Reason. 58(1), 149–179 (2017)MathSciNetCrossRef

27.

de Bruijn, N.: \(\lambda \)-calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church–Rosser theorem. Indag. Math 34(5), 381–392 (1972)MathSciNetCrossRef

28.

Charguéraud, A.: The locally nameless representation. J. Autom. Reason. 49(3), 363–408 (2012)MathSciNetCrossRef

29.

Chlipala, A.J.: Parametric higher-order abstract syntax for mechanized semantics. In: ICFP, pp. 143–156 (2008)

30.

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

31.

Copello, E., Szasz, N., Tasistro, Á.: Formalisation in constructive type theory of Barendregt’s variable convention for generic structures with binders. In: LFMTP, pp. 11–26 (2018)

32.

Curien, P.L.: Categorical combinators. Inf. Control 69(1–3), 188–254 (1986)MathSciNetCrossRef

33.

Despeyroux, J., Felty, A.P., Hirschowitz, A.: Higher-order abstract syntax in Coq. In: TLCA, pp. 124–138 (1995)

34.

van Doorn, F.: On the formalization of higher inductive types and synthetic homotopy theory. Ph.D. thesis, Carnegie Mellon University (2018)

35.

Felty, A.P., Momigliano, A.: Hybrid - A definitional two-level approach to reasoning with higher-order abstract syntax. J. Autom. Reason. 48(1), 43–105 (2012)CrossRef

36.

Felty, A.P., Momigliano, A., Pientka, B.: An open challenge problem repository for systems supporting binders. In: LFMTP, pp. 18–32 (2015)

37.

Felty, A.P., Pientka, B.: Reasoning with higher-order abstract syntax and contexts: a comparison. In: ITP, pp. 227–242 (2010)

38.

Ferreira, F., Pientka, B.: Programs using syntax with first-class binders. In: ESOP, pp. 504–529 (2017)

39.

Fiore, M., Gambino, N., Hyland, M., Winskel, G.: The cartesian closed bicategory of generalised species of structures. J. London Math. Soc. 1, 203–220 (2008)MathSciNetCrossRef

40.

Fiore, M., Plotkin, G., Turi, D.: Abstract syntax and variable binding (extended abstract). In: LICS, pp. 193–202 (1999)

41.

Gabbay, M., Pitts, A.M.: A new approach to abstract syntax involving binders. In: LICS, pp. 214–224 (1999)

42.

Gabbay, M., Pitts, A.M.: A new approach to abstract syntax with variable binding. Formal Asp. Comput. 13(3–5), 341–363 (2002)CrossRef

43.

Gabbay, M.J.: A general mathematics of names. Inf. Comput. 205(7), 982–1011 (2007)MathSciNetCrossRef

44.

Gambino, N., Hyland, M.: Wellfounded trees and dependent polynomial functors. In: TYPES, pp. 210–225 (2003)

45.

Gheri, L., Popescu, A.: A case study in reasoning about syntax with bindings: the Church–Rosser and standardization theorems. Submitted to the Journal of Automated Reasoning. http://andreipopescu.uk/papers/cbncbv.pdf

46.

Gheri, L., Popescu, A.: A general theory of syntax with bindings. Arch. Form. Proofs. (2019). http://isa-afp.org/entries/Binding_Syntax_Theory.html

47.

Gheri, L., Popescu, A.: A formalized general theory of syntax with bindings. In: ITP (2017)

48.

Gordon, A.D., Melham, T.F.: Five axioms of alpha-conversion. In: TPHOLs, pp. 173–190 (1996)

49.

Gunter, E.L., Osborn, C.J., Popescu, A.: Theory support for weak Higher Order Abstract Syntax in Isabelle/HOL. In: LFMTP, pp. 12–20 (2009)

50.

Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. In: LICS, pp. 194–204 (1987)

51.

Harrison, J.: Towards self-verification of HOL Light. In: IJCAR, pp. 177–191 (2006)

52.

Hennessy, M., Milner, R.: On observing nondeterminism and concurrency. In: ICALP, pp. 299–309 (1980)

53.

Hinze, R.: Polytypic programming with ease. J. Funct. Logic Program. 2001(3) (2001)

54.

Hirschowitz, A., Maggesi, M.: Modules over monads and initial semantics. Inf. Comput. 208(5), 545–564 (2010)MathSciNetCrossRef

55.

Hofmann, M.: Semantical analysis of higher-order abstract syntax. In: LICS (1999)

56.

Huet, G.P., Lang, B.: Proving and applying program transformations expressed with second-order patterns. Acta Inf. 11, 31–55 (1978). https://doi.org/10.1007/BF00264598 MathSciNetCrossRefMATH

57.

IsaFoL (Isabelle Formalization of Logic) project (2018). https://bitbucket.org/isafol/isafol/wiki/Home

58.

Joachimski, F.: Reduction properties of \(\varPi \text{IE}\)-systems. Ph.D. thesis, LMU München (2001)

59.

Kaiser, J., Schäfer, S., Stark, K.: Binder aware recursion over well-scoped De Bruijn syntax. In: CPP, pp. 293–306 (2018)

60.

Kammüller, F., Wenzel, M., Paulson, L.C.: Locales—a sectioning concept for Isabelle. In: TPHOLs, pp. 149–166 (1999)

61.

Keisler, H.J.: Model Theory for Infinitary Logic. North-Holland, Amsterdam (1971)MATH

62.

Keuchel, S., Jeuring, J.: Generic conversions of abstract syntax representations. In: Workshop on Generic Programming, pp. 57–68 (2012)

63.

Keuchel, S., Weirich, S., Schrijvers, T.: Needle & Knot: Binder boilerplate tied up. In: ESOP, pp. 419–445 (2016)

64.

Lee, G., Oliveira, B.C., Cho, S., Yi, K.: GMeta: a generic formal metatheory framework for first-order representations. In: ESOP, pp. 436–455 (2012)

65.

Licata, D.R., Harper, R.: A universe of binding and computation. In: ICFP ’09, pp. 123–134 (2009)

66.

Lochbihler, A.: Java and the Java memory model—a unified, machine-checked formalisation. In: H. Seidl (ed.) ESOP 2012, LNCS, vol. 7211, pp. 497–517. Springer, Berlin (2012)

67.

Luttik, B.: Choice quantification in process algebra. Ph.D. thesis, University of Amsterdam (2002)

68.

Miller, D., Tiu, A.: A proof theory for generic judgments. ACM Trans. Comput. Logic 6(4), 749–783 (2005)MathSciNetCrossRef

69.

Milner, R.: Communication and Concurrency. Prentice Hall, New York (1989)MATH

70.

Milner, R.: Communicating and Mobile Systems: The \(\pi \)-calculus. Cambridge University Press, Cambridge (2001)

71.

Nipkow, T., Klein, G.: Concrete Semantics: With Isabelle/HOL. Springer, Berlin (2014)CrossRef

72.

Nipkow, T., von Oheimb, D.: \(\text{ Java }{}_{{\rm light}}\) is type-safe - definitely. In: POPL, pp. 161–170 (1998)

73.

Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer, Berlin (2002)CrossRef

74.

Nordström, B., Petersson, K., Smith, J.M.: Programming in Martin-Löf’s Type Theory: An Introduction. Oxford University Press, Oxford (1990)MATH

75.

Norrish, M.: Mechanising lambda-calculus using a classical first order theory of terms with permutations. Higher-Order Symb. Comput. 19(2–3), 169–195 (2006)CrossRef

76.

Norrish, M., Vestergaard, R.: Proof pearl: De Bruijn terms really do work. In: TPHOLs, pp. 207–222 (2007)

77.

Paulson, L.C.: The foundation of a generic theorem prover. J. Autom. Reason. 5(3), 363–397 (1989)MathSciNetCrossRef

78.

Pfenning, F.: Computation and Deduction. Cambridge University Press, Cambridge (2001)

79.

Pfenning, F., Elliot, C.: Higher-order abstract syntax. In: PLDI, pp. 199–208 (1988)

80.

Pfenning, F., Elliott, C.: Higher-order abstract syntax. In: PLDI, pp. 199–208 (1988)

81.

Pfenning, F., Schürmann, C.: System description: Twelf–A meta-logical framework for deductive systems. In: CADE, pp. 202–206 (1999)

82.

Pientka, B.: Beluga: Programming with dependent types, contextual data, and contexts. In: FLOPS, pp. 1–12 (2010)

83.

Pitts, A.M.: Nominal logic: A first order theory of names and binding. In: TACS, pp. 219–242 (2001)

84.

Pitts, A.M.: Alpha-structural recursion and induction. J. ACM 53, 3 (2006)MathSciNetCrossRef

85.

Plotkin, G.D.: Call-by-name, call-by-value and the lambda-calculus. Theor. Comput. Sci. 1(2), 125–159 (1975)CrossRef

86.

Pollack, R.: Closure under alpha-conversion. In: TYPES, pp. 313–332 (1993)

87.

Pollack, R., Sato, M., Ricciotti, W.: A canonical locally named representation of binding. J. Autom. Reason. 49(2), 185–207 (2012)MathSciNetCrossRef

88.

Polonowski, E.: Automatically generated infrastructure for de Bruijn syntaxes. In: ITP, pp. 402–417 (2013)

89.

Popescu, A.: Contributions to the theory of syntax with bindings and to process algebra (2010). PhD thesis, Univ. of Illinois

90.

Popescu, A., Gunter, E.L.: Incremental pattern-based coinduction for process algebra and its Isabelle formalization. In: FoSSaCS (2010)

91.

Popescu, A., Gunter, E.L.: Recursion principles for syntax with bindings and substitution. In: ICFP, pp. 346–358 (2011)

92.

Popescu, A., Gunter, E.L., Osborn, C.J.: Strong normalization of System F by HOAS on top of FOAS. In: LICS, pp. 31–40 (2010)

93.

Popescu, A., Hölzl, J., Nipkow, T.: Proving concurrent noninterference. In: CPP, pp. 109–125 (2012)

94.

Popescu, A., Hölzl, J., Nipkow, T.: Formalizing probabilistic noninterference. In: CPP, pp. 259–275 (2013)

95.

Popescu, A., Roşu, G.: Term-generic logic. Theor. Comput. Sci. 577, 1–24 (2015)MathSciNetCrossRef

96.

Poswolsky, A., Schürmann, C.: System description: Delphin–a functional programming language for deductive systems. Electr. Notes Theor. Comput. Sci. 228, 113–120 (2009)CrossRef

97.

Rossberg, A., Russo, C.V., Dreyer, D.: F-ing modules. In: TLDI, pp. 89–102 (2010)

98.

Schäfer, S., Tebbi, T., Smolka, G.: Autosubst: reasoning with De Bruijn terms and parallel substitutions. In: ITP (2015)

99.

Schropp, A., Popescu, A.: Nonfree datatypes in Isabelle/HOL–animating a many-sorted metatheory. In: CPP, pp. 114–130 (2013)

100.

Schurmann, C., Despeyroux, J., Pfenning, F.: Primitive recursion for higher-order abstract syntax. Theor. Comput. Sci. 266(1–2), 1–57 (2001)MathSciNetCrossRef

101.

Sewell, P., Nardelli, F.Z., Owens, S., Peskine, G., Ridge, T., Sarkar, S., Strnisa, R.: Ott: effective tool support for the working semanticist. J. Funct. Program. 20(1), 71–122 (2010)CrossRef

102.

Stark, K., Schäfer, S., Kaiser, J.: Autosubst 2: reasoning with multi-sorted De Bruijn terms and vector substitutions. In: CPP (2019). To appear

103.

Stoughton, A.: Substitution revisited. Theor. Comput. Sci. 59, 317–325 (1988)MathSciNetCrossRef

104.

Sun, Y.: An algebraic generalization of frege structures-binding algebras. Theor. Comput. Sci. 211(1–2), 189–232 (1999)MathSciNetCrossRef

105.

Takahashi, M.: Parallel reductions in lambda-calculus. Inf. Comput. 118(1), 120–127 (1995)MathSciNetCrossRef

106.

Traytel, D., Popescu, A., Blanchette, J.C.: Foundational, compositional (co)datatypes for higher-order logic: category theory applied to theorem proving. In: LICS, pp. 596–605 (2012)

107.

The POPLmark challenge (2009). https://www.seas.upenn.edu/~plclub/poplmark/

108.

Urban, C.: Nominal techniques in Isabelle/HOL. J. Autom. Reason. 40(4), 327–356 (2008)MathSciNetCrossRef

109.

Urban, C., Berghofer, S.: A recursion combinator for nominal datatypes implemented in Isabelle/HOL. In: IJCAR, pp. 498–512 (2006)

110.

Urban, C., Berghofer, S., Norrish, M.: Barendregt’s variable convention in rule inductions. In: CADE, pp. 35–50 (2007)

111.

Urban, C., Kaliszyk, C.: General bindings and alpha-equivalence in Nominal Isabelle. In: ESOP, pp. 480–500 (2011)

112.

Urban, C., Tasson, C.: Nominal techniques in Isabelle/HOL. In: CADE, pp. 38–53 (2005)

Title: A Formalized General Theory of Syntax with Bindings: Extended Version
Authors: Lorenzo Gheri
Andrei Popescu
Publication date: 16-04-2019
Publisher: Springer Netherlands
Published in: Journal of Automated Reasoning / Issue 4/2020
Print ISSN: 0168-7433
Electronic ISSN: 1573-0670
DOI: https://doi.org/10.1007/s10817-019-09522-2

Springer Professional

Abstract

Please log in to get access to your license.

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

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Other articles of this Issue 4/2020

An Assertional Proof of Red–Black Trees Using Dafny

Automated Reasoning with Power Maps

Formalizing the Cox–Ross–Rubinstein Pricing of European Derivatives in Isabelle/HOL

Homogeneous Length Functions on Groups: Intertwined Computer and Human Proofs

A Verified Implementation of the Berlekamp–Zassenhaus Factorization Algorithm

Premium Partner