Email Gateway (Aug 22 2022 at 13:49): Email Gateway (Aug 22 2022 at 13:49):From: Corey Richardson <corey@octayn.net>
Ken Kubota <mail@kenkubota.de> writes:
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
Last updated: Apr 25 2024 at 01:08 UTC