Rensets and renaming-based recursion for syntax with bindings extended version
From MaRDI portal
Publication:6111524
DOI10.1007/S10817-023-09672-4OpenAlexW4383218038MaRDI QIDQ6111524
No author found.
Publication date: 4 August 2023
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-023-09672-4
Related Items (1)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
- The lambda calculus. Its syntax and semantics. Rev. ed.
- Nominal techniques in Isabelle/HOL
- Capture-avoiding substitution as a nominal algebra
- Substitution revisited
- An algebraic generalization of Frege structures -- binding algebras
- Isabelle/HOL. A proof assistant for higher-order logic
- The foundation of a generic theorem prover
- Nominal logic, a first order theory of names and binding
- The locally nameless representation
- Some lambda calculus and type theory formalized
- A formalized general theory of syntax with bindings: extended version
- Rensets and renaming-based recursion for syntax with bindings
- Term-generic logic
- Locales: a module system for mathematical theories
- A canonical locally named representation of binding
- Nominal Sets
- Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions
- Programs Using Syntax with First-Class Binders
- Engineering formal metatheory
- One-and-a-halfth-order Logic
- Alpha-structural recursion and induction
- Barendregt’s Variable Convention in Rule Inductions
- A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL
- Quotients of decidable objects in a topos
- A framework for defining logics
- de Bruijn notation as a nested datatype
- A general formulation of simultaneous inductive-recursive definitions in type theory
- A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
- POPLMark reloaded: Mechanizing proofs by logical relations
- Recursion principles for syntax with bindings and substitution
- Parametric higher-order abstract syntax for mechanized semantics
- Abella: A System for Reasoning about Relational Specifications
- Automated Deduction – CADE-20
- Homotopy Type Theory: Univalent Foundations of Mathematics
- Theorem Proving in Higher Order Logics
- Nominal Renaming Sets
- General Bindings and Alpha-Equivalence in Nominal Isabelle
- Primitive recursion for higher-order abstract syntax
- Rensets and renaming-based recursion for syntax with bindings extended version
This page was built for publication: Rensets and renaming-based recursion for syntax with bindings extended version
