A formalized general theory of syntax with bindings: extended version
From MaRDI portal
Publication:1984791
DOI10.1007/s10817-019-09522-2zbMath1468.68073OpenAlexW2935704972WikidataQ128037242 ScholiaQ128037242MaRDI QIDQ1984791
Publication date: 7 April 2020
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-019-09522-2
Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Formalization of mathematics in connection with theorem provers (68V20)
Related Items (6)
Rensets and renaming-based recursion for syntax with bindings extended version ⋮ Variable binding and substitution for (nameless) dummies ⋮ Variable binding and substitution for (nameless) dummies ⋮ Isabelle's metalogic: formalization and proof checker ⋮ Rensets and renaming-based recursion for syntax with bindings ⋮ A formalization and proof checker for Isabelle's metalogic
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
- A new approach to abstract syntax with variable binding
- Mechanising \(\lambda\)-calculus using a classical first order theory of terms with permutations
- Nominal techniques in Isabelle/HOL
- Modules over monads and initial semantics
- Substitution revisited
- Call-by-name, call-by-value and the \(\lambda\)-calculus
- Proving and applying program transformations expressed with second-order patterns
- An algebraic generalization of Frege structures -- binding algebras
- Isabelle/HOL. A proof assistant for higher-order logic
- Foundational (co)datatypes and (co)recursion for higher-order logic
- A formalized general theory of syntax with bindings
- The foundation of a generic theorem prover
- The locally nameless representation
- Term-generic logic
- Soundness and completeness proofs by coinductive methods
- A general mathematics of names
- A canonical locally named representation of binding
- Model theory for infinitary logic. Logic with countable conjunctions and finite quantifiers
- Mechanizing the Metatheory of Sledgehammer
- Truly Modular (Co)datatypes for Isabelle/HOL
- Cardinals in Isabelle/HOL
- GMeta: A Generic Formal Metatheory Framework for First-Order Representations
- Java and the Java Memory Model — A Unified, Machine-Checked Formalisation
- Concrete Semantics
- A universe of binding and computation
- Nonfree Datatypes in Isabelle/HOL
- Formalizing Probabilistic Noninterference
- Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions
- Foundational extensible corecursion: a proof assistant perspective
- Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving
- Friends with Benefits
- Programs Using Syntax with First-Class Binders
- Engineering formal metatheory
- Unified Classical Logic Completeness
- Proof Pearl: De Bruijn Terms Really Do Work
- Alpha-structural recursion and induction
- Incremental Pattern-Based Coinduction for Process Algebra and Its Isabelle Formalization
- Barendregt’s Variable Convention in Rule Inductions
- Towards Self-verification of HOL Light
- A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL
- Categorical combinators
- A framework for defining logics
- de Bruijn notation as a nested datatype
- Secure Communicating Systems
- Proving Concurrent Noninterference
- F-ing modules
- A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
- Recursion principles for syntax with bindings and substitution
- Parametric higher-order abstract syntax for mechanized semantics
- Ott: Effective tool support for the working semanticist
- Abella: A System for Reasoning about Relational Specifications
- A proof theory for generic judgments
- Encoding Monomorphic and Polymorphic Types
- Automatically Generated Infrastructure for De Bruijn Syntaxes
- Indexed containers
- Automated Deduction – CADE-20
- The cartesian closed bicategory of generalised species of structures
- Types for Proofs and Programs
- Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison
- Psi-calculi in Isabelle
- General Bindings and Alpha-Equivalence in Nominal Isabelle
- Parallel reductions in \(\lambda\)-calculus
- Primitive recursion for higher-order abstract syntax
This page was built for publication: A formalized general theory of syntax with bindings: extended version
