Sciweavers

TPHOL
1999
IEEE

Inductive Datatypes in HOL - Lessons Learned in Formal-Logic Engineering

13 years 8 months ago
Inductive Datatypes in HOL - Lessons Learned in Formal-Logic Engineering
Abstract. Isabelle/HOL has recently acquired new versions of definitional packages for inductive datatypes and primitive recursive functions. In contrast to its predecessors and most other implementations, Isabelle/HOL datatypes may be mutually and indirect recursive, even infinitely branching. We also support inverted datatype definitions for characterizing existing types as being inductive ones later. All our constructions are fully definitional according to established HOL tradition. Stepping back from the logical details, we also see this work as a typical example of what could be called "Formal-Logic Engineering". We observe that building realistic theorem proving environments involves further issues rather than pure logic only.
Stefan Berghofer, Markus Wenzel
Added 04 Aug 2010
Updated 04 Aug 2010
Type Conference
Year 1999
Where TPHOL
Authors Stefan Berghofer, Markus Wenzel
Comments (0)