A formalized general theory of syntax with bindings: extended version
From MaRDI portal
Recommendations
Cites work
- A canonical locally named representation of binding
- A formalized general theory of syntax with bindings
- A framework for defining logics
- A general mathematics of names
- A head-to-head comparison of de Bruijn indices and names
- A new approach to abstract syntax with variable binding
- A proof theory for generic judgments
- A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL
- A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
- A universe of binding and computation
- Abella: a system for reasoning about relational specifications
- Alpha-structural recursion and induction
- An algebraic generalization of Frege structures -- binding algebras
- Automated Deduction – CADE-20
- Automatically Generated Infrastructure for De Bruijn Syntaxes
- Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions
- Barendregt’s Variable Convention in Rule Inductions
- Call-by-name, call-by-value and the \(\lambda\)-calculus
- Cardinals in Isabelle/HOL
- Categorical combinators
- Concrete semantics. With Isabelle/HOL
- de Bruijn notation as a nested datatype
- Encoding monomorphic and polymorphic types
- Engineering formal metatheory
- F-ing modules
- Formalizing probabilistic noninterference
- Foundational (co)datatypes and (co)recursion for higher-order logic
- Foundational extensible corecursion: a proof assistant perspective
- 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
- GMeta: a generic formal metatheory framework for first-order representations
- scientific article; zbMATH DE number 2185657 (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 50149 (Why is no real title available?)
- scientific article; zbMATH DE number 1797606 (Why is no real title available?)
- scientific article; zbMATH DE number 1424012 (Why is no real title available?)
- scientific article; zbMATH DE number 1424053 (Why is no real title available?)
- scientific article; zbMATH DE number 3400430 (Why is no real title available?)
- scientific article; zbMATH DE number 2242589 (Why is no real title available?)
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
- Incremental pattern-based coinduction for process algebra and its Isabelle formalization
- Indexed containers
- 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
- Modules over monads and initial semantics
- 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
- Parallel reductions in \(\lambda\)-calculus
- Parametric higher-order abstract syntax for mechanized semantics
- Polytypic programming with ease
- Primitive recursion for higher-order abstract syntax
- Programs using syntax with first-class binders
- Proof Pearl: De Bruijn Terms Really Do Work
- Proving and applying program transformations expressed with second-order patterns
- Proving concurrent noninterference
- Psi-calculi in Isabelle
- Reasoning with higher-order abstract syntax and contexts: a comparison
- Recursion principles for syntax with bindings and substitution
- Secure Communicating Systems
- Soundness and completeness proofs by coinductive methods
- Substitution revisited
- Term-generic logic
- The cartesian closed bicategory of generalised species of structures
- The foundation of a generic theorem prover
- The locally nameless representation
- Towards Self-verification of HOL Light
- Truly modular (co)datatypes for Isabelle/HOL
- Types for Proofs and Programs
- Unified Classical Logic Completeness
Cited in
(18)- A formalized general theory of syntax with bindings
- Binding operators for nominal sets
- 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
- Mechanized metatheory revisited
- A canonical locally named representation of binding
- Substitution in non-wellfounded syntax with variable binding
- scientific article; zbMATH DE number 1476647 (Why is no real title available?)
- Recursion principles for syntax with bindings and substitution
- Flexary operators for formalized mathematics
- Types for Proofs and Programs
- 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
- A theory of binding structures and applications to rewriting
- Substitution in non-wellfounded syntax with variable binding
- On bounded interpretations of grammar forms
Describes a project that uses
Uses Software
This page was built for publication: A formalized general theory of syntax with bindings: extended version
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1984791)
