nach oben

nächster Artikel Homogeneous Length Functions on Groups: Intertw...

Tipp

A Formalized General Theory of Syntax with Bindings: Extended Version

Zeitschrift:: Journal of Automated Reasoning > Ausgabe 4/2020

Autoren:: Lorenzo Gheri, Andrei Popescu

» Jetzt Zugang zum Volltext erhalten

Wichtige Hinweise

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

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.

Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten

Jetzt einloggen Kostenlos registrieren

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

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

über 69.000 Bücher
über 500 Zeitschriften

aus folgenden Fachgebieten:

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

Testen Sie jetzt 30 Tage kostenlos.

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 58.000 Bücher
über 300 Zeitschriften

aus folgenden Fachgebieten:

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

Testen Sie jetzt 30 Tage kostenlos.

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 50.000 Bücher
über 380 Zeitschriften

aus folgenden Fachgebieten:

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

Testen Sie jetzt 30 Tage kostenlos.

Jetzt informieren

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)

Titel: A Formalized General Theory of Syntax with Bindings: Extended Version
Autoren:: Lorenzo Gheri
Andrei Popescu
Publikationsdatum: 16.04.2019
DOI: https://doi.org/10.1007/s10817-019-09522-2
Verlag: Springer Netherlands
Zeitschrift: Journal of Automated Reasoning
Ausgabe 4/2020
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670

Premium Partner

Bildnachweise

Springer Professional

Tipp

Weitere Artikel dieser Ausgabe durch Wischen aufrufen

Publisher's Note

Abstract

Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Weitere Artikel der Ausgabe 4/2020

Homogeneous Length Functions on Groups: Intertwined Computer and Human Proofs

Automated Reasoning with Power Maps

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

An Assertional Proof of Red–Black Trees Using Dafny

A Verified Implementation of the Berlekamp–Zassenhaus Factorization Algorithm

Premium Partner