Rensets and renaming-based recursion for syntax with bindings
From MaRDI portal
Publication:2104549
DOI10.1007/978-3-031-10769-6_36OpenAlexW4289104030MaRDI QIDQ2104549
Publication date: 7 December 2022
Full work available at URL: https://arxiv.org/abs/2205.09233
Related Items (1)
Uses Software
Cites Work
- 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
- 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
- A formalized general theory of syntax with bindings: extended version
- Term-generic logic
- A canonical locally named representation of binding
- Nominal Sets
- Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions
- Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving
- Programs Using Syntax with First-Class Binders
- Programming Inductive Proofs
- 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
This page was built for publication: Rensets and renaming-based recursion for syntax with bindings