Witnessing (Co)datatypes

Abstract : Datatypes and codatatypes are useful for specifying and reasoning about (possibly infinite) computational processes. The Isabelle/HOL proof assistant has recently been extended with a definitional package that supports both. We describe a complete procedure for deriving nonemptiness witnesses in the general mutually recursive, nested case—nonemptiness being a proviso for introducing types in higher-order logic.
Document type :
Conference papers
Complete list of metadatas

Cited literature [38 references]  Display  Hide  Download

https://hal.inria.fr/hal-01212587
Contributor : Jasmin Blanchette <>
Submitted on : Wednesday, October 7, 2015 - 3:27:01 PM
Last modification on : Tuesday, February 19, 2019 - 3:40:03 PM
Long-term archiving on : Friday, January 8, 2016 - 10:15:52 AM

File

wit.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel. Witnessing (Co)datatypes. ESOP 2015, Apr 2015, London, United Kingdom. ⟨10.1007/978-3-662-46669-8_15⟩. ⟨hal-01212587⟩

Share

Metrics

Record views

202

Files downloads

88