# [isabelle] Declaration of (co)datatypes (was: Some corrections and amendments)

Ken Kubota <mail at kenkubota.de> writes:
> This is, of course, correct, but doesn't justify the specific mode of type
> introduction used here, namely the Backus-Naur form (BNF). The BNF was designed
> to specify formal grammars in computer science, but (mathematical) types are
> objects that must have certain logical properties, such as being non-empty.
> Thus the introduction of additional mathematical types should be subject to
> proof, and not a matter of mere declaration via the BNF.
>
The datatype declarations written in theory files is surface syntax for
the underlying datatype package which handles proving non-emptiness
among many other properties. The ML-style declaration is a convenient
abstraction that is easy to use. The following paper explains the
underlying principles:
Dmitry Traytel, Andrei Popescu, and Jasmin C. Blanchette. 2012.
Foundational, Compositional (Co)datatypes for Higher-Order Logic:
Category Theory Applied to Theorem Proving. In Proceedings of the 2012
27th Annual IEEE/ACM Symposium on Logic in Computer Science (LICS '12).
IEEE Computer Society, Washington, DC, USA, 596-605.
DOI=http://dx.doi.org/10.1109/LICS.2012.75
There are additional references at the end of the tutorial for the
datatype package,
https://isabelle.in.tum.de/dist/Isabelle2016/doc/datatypes.pdf
--
cmr
+610481782084
http://octayn.net/

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*