A formalized general theory of syntax with bindings: extended version
type: Item
instance of: scholarly article
title: A formalized general theory of syntax with bindings: extended version
zbMATH Open document ID: 1468.68073
author: Yanyan Li
published in: Journal of Automated Reasoning
publication date: 2020-04-07T00:00:00Z
Mathematics Subject Classification ID: 68N30
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68V20
zbMATH DE Number: 7187041
zbMATH Keywords: syntax with bindings
zbMATH Keywords: recursion and induction principles
zbMATH Keywords: Isabelle/HOL
describes a project that uses: PoplMark
describes a project that uses: HOL
describes a project that uses: HoTT
describes a project that uses: AmiCo
describes a project that uses: HYBRID
describes a project that uses: Isabelle
describes a project that uses: Ott
describes a project that uses: Psi-calculi
describes a project that uses: Isabelle/HOL
describes a project that uses: Twelf
describes a project that uses: Abella
describes a project that uses: Gmeta
describes a project that uses: LNgen
describes a project that uses: Nominal Isabelle
describes a project that uses: Locales
describes a project that uses: Delphin
MaRDI profile type: Publication
full work available at URL: s10817-019-09522-2
OpenAlex ID: W2935704972
cites work: A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
cites work: Indexed containers
cites work: Q4945244
cites work: Nominal reasoning techniques in Coq (extended abstract)
cites work: Engineering formal metatheory
cites work: Abella: A System for Reasoning about Relational Specifications
cites work: Psi-calculi in Isabelle
cites work: A head-to-head comparison of de Bruijn indices and names
cites work: Q4945200
cites work: de Bruijn notation as a nested datatype
cites work: Encoding Monomorphic and Polymorphic Types
cites work: Friends with Benefits
cites work: Truly Modular (Co)datatypes for Isabelle/HOL
cites work: Foundational (co)datatypes and (co)recursion for higher-order logic
cites work: Mechanizing the Metatheory of Sledgehammer
cites work: Cardinals in Isabelle/HOL
cites work: Unified Classical Logic Completeness
cites work: Foundational extensible corecursion: a proof assistant perspective
cites work: Soundness and completeness proofs by coinductive methods
cites work: Q5667469
cites work: The locally nameless representation
cites work: Parametric higher-order abstract syntax for mechanized semantics
cites work: Categorical combinators
cites work: Q3024831
cites work: Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
cites work: Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison
cites work: Programs Using Syntax with First-Class Binders
cites work: The cartesian closed bicategory of generalised species of structures
cites work: A new approach to abstract syntax with variable binding
cites work: A general mathematics of names
cites work: Types for Proofs and Programs
cites work: A formalized general theory of syntax with bindings
cites work: A framework for defining logics
cites work: Towards Self-verification of HOL Light
cites work: Q3883467
cites work: Polytypic programming with ease
cites work: Modules over monads and initial semantics
cites work: Proving and applying program transformations expressed with second-order patterns
cites work: Q4552763
cites work: Model theory for infinitary logic. Logic with countable conjunctions and finite quantifiers
cites work: GMeta: A Generic Formal Metatheory Framework for First-Order Representations
cites work: A universe of binding and computation
cites work: Java and the Java Memory Model — A Unified, Machine-Checked Formalisation
cites work: A proof theory for generic judgments
cites work: Q3992568
cites work: Secure Communicating Systems
cites work: Concrete Semantics

A formalized general theory of syntax with bindings: extended version (cites work)
cites work: Isabelle/HOL. A proof assistant for higher-order logic

A formalized general theory of syntax with bindings: extended version (cites work)
cites work: Q3999860

A formalized general theory of syntax with bindings: extended version (cites work)
cites work: Mechanising \(\lambda\)-calculus using a classical first order theory of terms with permutations

A formalized general theory of syntax with bindings: extended version (cites work)
cites work: Proof Pearl: De Bruijn Terms Really Do Work

A formalized general theory of syntax with bindings: extended version (cites work)
cites work: The foundation of a generic theorem prover

A formalized general theory of syntax with bindings: extended version (cites work)
cites work: Q5714442

A formalized general theory of syntax with bindings: extended version (cites work)
cites work: Alpha-structural recursion and induction

A formalized general theory of syntax with bindings: extended version (cites work)
cites work: Call-by-name, call-by-value and the \(\lambda\)-calculus

A formalized general theory of syntax with bindings: extended version (cites work)
cites work: A canonical locally named representation of binding

A formalized general theory of syntax with bindings: extended version (cites work)
cites work: Automatically Generated Infrastructure for De Bruijn Syntaxes

A formalized general theory of syntax with bindings: extended version (cites work)
cites work: Incremental Pattern-Based Coinduction for Process Algebra and Its Isabelle Formalization

A formalized general theory of syntax with bindings: extended version (cites work)
cites work: Recursion principles for syntax with bindings and substitution

A formalized general theory of syntax with bindings: extended version (cites work)
cites work: Proving Concurrent Noninterference

A formalized general theory of syntax with bindings: extended version (cites work)
cites work: Formalizing Probabilistic Noninterference

A formalized general theory of syntax with bindings: extended version (cites work)
cites work: Term-generic logic

A formalized general theory of syntax with bindings: extended version (cites work)
cites work: F-ing modules

A formalized general theory of syntax with bindings: extended version (cites work)
cites work: Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions

A formalized general theory of syntax with bindings: extended version (cites work)
cites work: Nonfree Datatypes in Isabelle/HOL

A formalized general theory of syntax with bindings: extended version (cites work)
cites work: Primitive recursion for higher-order abstract syntax

A formalized general theory of syntax with bindings: extended version (cites work)
cites work: Ott: Effective tool support for the working semanticist

A formalized general theory of syntax with bindings: extended version (cites work)
cites work: Substitution revisited

A formalized general theory of syntax with bindings: extended version (cites work)
cites work: An algebraic generalization of Frege structures -- binding algebras

A formalized general theory of syntax with bindings: extended version (cites work)
cites work: Parallel reductions in \(\lambda\)-calculus

A formalized general theory of syntax with bindings: extended version (cites work)
cites work: Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving

A formalized general theory of syntax with bindings: extended version (cites work)
cites work: Nominal techniques in Isabelle/HOL

A formalized general theory of syntax with bindings: extended version (cites work)
cites work: A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL

A formalized general theory of syntax with bindings: extended version (cites work)
cites work: Barendregt’s Variable Convention in Rule Inductions

A formalized general theory of syntax with bindings: extended version (cites work)
cites work: General Bindings and Alpha-Equivalence in Nominal Isabelle

A formalized general theory of syntax with bindings: extended version (cites work)
cites work: Automated Deduction – CADE-20

A formalized general theory of syntax with bindings: extended version (Wikidata QID)
Wikidata QID: Q128037242

A formalized general theory of syntax with bindings: extended version (DOI)
DOI: 10.1007/S10817-019-09522-2