A recursion combinator for nominal datatypes implemented in Isabelle/HOL

Christian Urban, S. Berghofer

Research output: Chapter in Book/Report/Conference proceedingOther chapter contribution

29 Citations (Scopus)


The nominal datatype package implements an infrastructure in Isabelle/HOL for defining languages involving binders and for reasoning conveniently about alpha-equivalence classes. Pitts stated some general conditions under which functions over alpha-equivalence classes can be defined by a form of structural recursion and gave a clever proof for the existence of a primitive-recursion combinator. We give a version of this proof that works directly over nominal datatypes and does not rely upon auxiliary constructions. We further introduce proving tools and a heuristic that made the automation of our proof tractable. This automation is an essential prerequisite for the nominal datatype package to become useful.
Original languageEnglish
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Number of pages15
Volume4130 LNAI
Publication statusPublished - 1 Jan 2006


Dive into the research topics of 'A recursion combinator for nominal datatypes implemented in Isabelle/HOL'. Together they form a unique fingerprint.

Cite this