Witnessing (Co)datatypes - Archive ouverte HAL Access content directly
Conference Papers Year : 2015

Witnessing (Co)datatypes

(1, 2) , (3) , (4)
1
2
3
4

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.
Fichier principal
Vignette du fichier
wit.pdf (255.77 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01212587 , version 1 (07-10-2015)

Identifiers

Cite

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⟩
130 View
77 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More