Rensets and renaming-based recursion for syntax with bindings
From MaRDI portal
Publication:2104549
DOI10.1007/978-3-031-10769-6_36OpenAlexW4289104030MaRDI QIDQ2104549FDOQ2104549
Publication date: 7 December 2022
Full work available at URL: https://arxiv.org/abs/2205.09233
Cites Work
- Abella: A System for Reasoning about Relational Specifications
- Nominal techniques in Isabelle/HOL
- Isabelle/HOL. A proof assistant for higher-order logic
- Nominal logic, a first order theory of names and binding
- Nominal sets. Names and symmetry in computer science
- Alpha-structural recursion and induction
- A framework for defining logics
- The lambda calculus. Its syntax and semantics. Rev. ed.
- Homotopy Type Theory: Univalent Foundations of Mathematics
- The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
- Programming Inductive Proofs
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
- Title not available (Why is that?)
- General bindings and alpha-equivalence in Nominal Isabelle
- An algebraic generalization of Frege structures -- binding algebras
- Nominal Renaming Sets
- A head-to-head comparison of de Bruijn indices and names
- Title not available (Why is that?)
- A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL
- Parametric higher-order abstract syntax for mechanized semantics
- Automated Deduction – CADE-20
- Theorem Proving in Higher Order Logics
- Primitive recursion for higher-order abstract syntax
- Title not available (Why is that?)
- The locally nameless representation
- de Bruijn notation as a nested datatype
- A general formulation of simultaneous inductive-recursive definitions in type theory
- Title not available (Why is that?)
- The foundation of a generic theorem prover
- A formalized general theory of syntax with bindings: extended version
- A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
- POPLMark reloaded: Mechanizing proofs by logical relations
- Barendregt’s Variable Convention in Rule Inductions
- A canonical locally named representation of binding
- Quotients of decidable objects in a topos
- Title not available (Why is that?)
- Title not available (Why is that?)
- Term-generic logic
- Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving
- Recursion principles for syntax with bindings and substitution
- Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions
- Programs Using Syntax with First-Class Binders
Cited In (2)
Uses Software
This page was built for publication: Rensets and renaming-based recursion for syntax with bindings
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2104549)
