Rensets and renaming-based recursion for syntax with bindings
From MaRDI portal
Publication:2104549
Cites work
- scientific article; zbMATH DE number 6694181 (Why is no real title available?)
- scientific article; zbMATH DE number 2185657 (Why is no real title available?)
- scientific article; zbMATH DE number 3722625 (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?)
- A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL
- A canonical locally named representation of binding
- A formalized general theory of syntax with bindings: extended version
- A framework for defining logics
- A general formulation of simultaneous inductive-recursive definitions in type theory
- A head-to-head comparison of de Bruijn indices and names
- A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
- 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
- Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions
- Barendregt’s Variable Convention in Rule Inductions
- Foundational, compositional (co)datatypes for higher-order logic: category theory applied to theorem proving
- General bindings and alpha-equivalence in Nominal Isabelle
- Homotopy type theory. Univalent foundations of mathematics
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
- Isabelle/HOL. A proof assistant for higher-order logic
- Nominal Renaming Sets
- Nominal logic, a first order theory of names and binding
- Nominal presentation of cubical sets models of type theory
- Nominal sets. Names and symmetry in computer science
- Nominal techniques in Isabelle/HOL
- POPLMark reloaded: mechanizing proofs by logical relations
- Parametric higher-order abstract syntax for mechanized semantics
- Primitive recursion for higher-order abstract syntax
- Programming inductive proofs. A new approach based on contextual types
- Programs using syntax with first-class binders
- Quotients of decidable objects in a topos
- Recursion principles for syntax with bindings and substitution
- Term-generic logic
- The foundation of a generic theorem prover
- The lambda calculus. Its syntax and semantics. Rev. ed.
- The locally nameless representation
- The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
- Theorem Proving in Higher Order Logics
- de Bruijn notation as a nested datatype
Cited in
(2)
Describes a project that uses
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)
