A formalized general theory of syntax with bindings

DOI10.1007/978-3-319-66107-0_16MaRDI QIDQ1687739zbMATH OpenOpenAlexFDO

Authors Peng Zhang

Publication date 4 January 2018

Full work available at URL https://arxiv.org/abs/1707.00024, https://eprints.mdx.ac.uk/22102/6/bindings.pdf

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Formalization of mathematics in connection with theorem provers (68V20)

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 includes a rich collection of properties of the standard operators on terms, such as substitution and freshness. It also includes induction and recursion principles and support for semantic interpretation, all tailored for smooth interaction with the bindings and the standard operators.

Recommendations

• A formalized general theory of syntax with bindings: extended version
• Binding operators for nominal sets
• Recursion principles for syntax with bindings and substitution
• A new approach to abstract syntax with variable binding
• Substitution in non-wellfounded syntax with variable binding

Cites work

• scientific article; zbMATH DE number 2185657 (Why is no real title available?)
• scientific article; zbMATH DE number 3889501 (Why is no real title available?)
• scientific article; zbMATH DE number 3688686 (Why is no real title available?)
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 1424012 (Why is no real title available?)
• scientific article; zbMATH DE number 2242589 (Why is no real title available?)
• A Brief Overview of HOL4
• A formalized general theory of syntax with bindings
• A framework for defining logics
• A general mathematics of names
• A proof theory for generic judgments
• Alpha-structural recursion and induction
• An algebraic generalization of Frege structures -- binding algebras
• Automated Deduction – CADE-20
• Barendregt’s Variable Convention in Rule Inductions
• Cardinals in Isabelle/HOL
• Concrete semantics. With Isabelle/HOL
• Encoding monomorphic and polymorphic types
• Engineering formal metatheory
• Formalizing probabilistic noninterference
• Foundational extensible corecursion: a proof assistant perspective
• Foundational nonuniform (co)datatypes for higher-order logic
• Foundational, compositional (co)datatypes for higher-order logic: category theory applied to theorem proving
• Friends with benefits. Implementing corecursion in foundational proof assistants
• General bindings and alpha-equivalence in Nominal Isabelle
• Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
• Incremental pattern-based coinduction for process algebra and its Isabelle formalization
• Isabelle/HOL. A proof assistant for higher-order logic
• Java and the Java memory model -- a unified, machine-checked formalisation
• Mechanising \(\lambda\)-calculus using a classical first order theory of terms with permutations
• Mechanizing the metatheory of Sledgehammer
• Model theory for infinitary logic. Logic with countable conjunctions and finite quantifiers
• Nested abstract syntax in Coq
• Nominal reasoning techniques in Coq (extended abstract)
• Nominal techniques in Isabelle/HOL
• Nonfree datatypes in Isabelle/HOL. Animating a many-sorted metatheory
• Ott: Effective tool support for the working semanticist
• Parametric higher-order abstract syntax for mechanized semantics
• Proof Pearl: De Bruijn Terms Really Do Work
• Proving concurrent noninterference
• Psi-calculi in Isabelle
• Recursion principles for syntax with bindings and substitution
• Secure Communicating Systems
• Soundness and completeness proofs by coinductive methods
• Term-generic logic
• Truly modular (co)datatypes for Isabelle/HOL
• Unified Classical Logic Completeness

Cited in

(11)

• A theory of binding structures and applications to rewriting
• Substitution in non-wellfounded syntax with variable binding
• Substitution in non-wellfounded syntax with variable binding
• Binding operators for nominal sets
• Mechanized metatheory revisited
• A formalized general theory of syntax with bindings
• Types for Proofs and Programs
• A formalized general theory of syntax with bindings: extended version
• A NEW APPROACH TO FORMAL SYNTAX
• Recursion principles for syntax with bindings and substitution
• On bounded interpretations of grammar forms

This page was built for publication: A formalized general theory of syntax with bindings

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1687739)