A formalized general theory of syntax with bindings
From MaRDI portal
Publication:1687739
DOI10.1007/978-3-319-66107-0_16zbMath1468.68072arXiv1707.00024OpenAlexW2730334049MaRDI QIDQ1687739
Publication date: 4 January 2018
Full work available at URL: https://arxiv.org/abs/1707.00024
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 (2)
A formalized general theory of syntax with bindings ⋮ A formalized general theory of syntax with bindings: extended version
Cites Work
- 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
- Mechanising \(\lambda\)-calculus using a classical first order theory of terms with permutations
- Nominal techniques in Isabelle/HOL
- An algebraic generalization of Frege structures -- binding algebras
- Isabelle/HOL. A proof assistant for higher-order logic
- A formalized general theory of syntax with bindings
- Nested abstract syntax in Coq
- Term-generic logic
- Soundness and completeness proofs by coinductive methods
- A general mathematics of names
- 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
- Java and the Java Memory Model — A Unified, Machine-Checked Formalisation
- Concrete Semantics
- Nonfree Datatypes in Isabelle/HOL
- Formalizing Probabilistic Noninterference
- Foundational extensible corecursion: a proof assistant perspective
- Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving
- Friends with Benefits
- Engineering formal metatheory
- Unified Classical Logic Completeness
- Proof Pearl: De Bruijn Terms Really Do Work
- A Brief Overview of HOL4
- Alpha-structural recursion and induction
- Incremental Pattern-Based Coinduction for Process Algebra and Its Isabelle Formalization
- Barendregt’s Variable Convention in Rule Inductions
- A framework for defining logics
- Secure Communicating Systems
- Proving Concurrent Noninterference
- Recursion principles for syntax with bindings and substitution
- Parametric higher-order abstract syntax for mechanized semantics
- Ott: Effective tool support for the working semanticist
- A proof theory for generic judgments
- Encoding Monomorphic and Polymorphic Types
- Automated Deduction – CADE-20
- Psi-calculi in Isabelle
- General Bindings and Alpha-Equivalence in Nominal Isabelle
This page was built for publication: A formalized general theory of syntax with bindings
