A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL
From MaRDI portal
Publication:3613430
DOI10.1007/11814771_41zbMath1222.68374OpenAlexW2162208777MaRDI QIDQ3613430
Christian Urban, Stefan Berghofer
Publication date: 12 March 2009
Published in: Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/11814771_41
Related Items
Formalising FinFuns – Generating Code for Functions as Data from Isabelle/HOL ⋮ Rensets and renaming-based recursion for syntax with bindings extended version ⋮ Nominal Sets in Agda - A Fresh and Immature Mechanization ⋮ Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax ⋮ Nominal techniques in Isabelle/HOL ⋮ A formalized general theory of syntax with bindings: extended version ⋮ Formal SOS-Proofs for the Lambda-Calculus ⋮ A Simple Nominal Type Theory ⋮ Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theorem ⋮ Nominal Equational Logic ⋮ Rensets and renaming-based recursion for syntax with bindings ⋮ Abstract Syntax: Substitution and Binders ⋮ Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention
Uses Software
