Skip to Main content Skip to Navigation
Conference papers

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 metadata

Cited literature [38 references]  Display  Hide  Download
Contributor : Jasmin Blanchette Connect in order to contact the contributor
Submitted on : Wednesday, October 7, 2015 - 3:27:01 PM
Last modification on : Thursday, January 6, 2022 - 11:38:04 AM
Long-term archiving on: : Friday, January 8, 2016 - 10:15:52 AM


Files produced by the author(s)




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⟩



Les métriques sont temporairement indisponibles