Rensets and renaming-based recursion for syntax with bindings

DOI10.1007/978-3-031-10769-6_36OpenAlexW4289104030MaRDI QIDQ2104549

Yanyan Li

Publication date: 7 December 2022

Full work available at URL: https://arxiv.org/abs/2205.09233

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (1)

Rensets and renaming-based recursion for syntax with bindings extended version

Uses Software

• HYBRID
• Beluga
• Isabelle/HOL
• Twelf
• Abella
• PoplMark
• Nominal Isabelle
• Autosubst

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