Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Journal of Automated Reasoning
Erschienen in: Journal of Automated Reasoning 4/2020

16.04.2019

A Formalized General Theory of Syntax with Bindings: Extended Version

verfasst von: Lorenzo Gheri, Andrei Popescu

Erschienen in: Journal of Automated Reasoning | Ausgabe 4/2020

Einloggen

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

search-config
loading …

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.
Nächster Artikel Homogeneous Length Functions on Groups: Intertwined Computer and Human Proofs

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

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

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

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

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

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

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




Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

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




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren
Fußnoten
1
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].
 
2
This is a contrived example, where no “real” recursion occurs—but it illustrates the point.
 
3
Note that requiring \(|{\textsf {vars}}{\textsf {Of}}\;p| < |\mathbf{var}|\) is the same as requiring that \({\textsf {vars}}{\textsf {Of}}\;p\) be finite.
 
4
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.
 
5
This work was the first entry in the (today very prolific) IsaFoL project [57].
 
6
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.
 
7
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].
 
8
The difficulties of achieving this with nominal logic recursion are analyzed in [84, §6.3].
 
Literatur
1.
Abel, A., Momigliano, A., Pientka, B.: POPLMark Reloaded. In: LFMTP (2017)
2.
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)
3.
Allais, G., Chapman, J., McBride, C., McKinna, J.: Type-and-scope safe programs and their proofs. In: CPP, pp. 195–207 (2017)
4.
Altenkirch, T., Ghani, N., Hancock, P., McBride, C., Morris, P.: Indexed containers. J. Funct. Program. 25, (2015)
5.
Altenkirch, T., Reus, B.: Monadic presentations of lambda terms using generalized inductive types. In: CSL, pp. 453–468 (1999)
6.
Aydemir, B., Weirich, S.: LNgen: Tool support for locally nameless representations. Tech. rep., UPenn (2010)
7.
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
8.
Aydemir, B.E., Charguéraud, A., Pierce, B.C., Pollack, R., Weirich, S.: Engineering formal metatheory. In: POPL, pp. 3–15 (2008)
9.
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.
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.
16.
Blanchette, J.C., Böhme, S., Popescu, A., Smallbone, N.: Encoding monomorphic and polymorphic types. In: TACAS, pp. 493–507 (2013)
17.
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.
29.
Chlipala, A.J.: Parametric higher-order abstract syntax for mechanized semantics. In: ICFP, pp. 143–156 (2008)
30.
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.
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.
44.
Gambino, N., Hyland, M.: Wellfounded trees and dependent polynomial functors. In: TYPES, pp. 210–225 (2003)
45.
46.
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.
57.
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.
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.
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.
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.
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.
104.
Sun, Y.: An algebraic generalization of frege structures-binding algebras. Theor. Comput. Sci. 211(1–2), 189–232 (1999)MathSciNetCrossRef
105.
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.
108.
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)
Metadaten
Titel
A Formalized General Theory of Syntax with Bindings: Extended Version
verfasst von
Lorenzo Gheri
Andrei Popescu
Publikationsdatum
16.04.2019
Verlag
Springer Netherlands
Erschienen in
Journal of Automated Reasoning / Ausgabe 4/2020
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI
https://doi.org/10.1007/s10817-019-09522-2

Weitere Artikel der Ausgabe 4/2020

Journal of Automated Reasoning 4/2020 Zur Ausgabe

OriginalPaper

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

OriginalPaper

An Assertional Proof of Red–Black Trees Using Dafny

OriginalPaper

Automated Reasoning with Power Maps

OriginalPaper

A Verified Implementation of the Berlekamp–Zassenhaus Factorization Algorithm

OriginalPaper

Homogeneous Length Functions on Groups: Intertwined Computer and Human Proofs