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.
Type de document :
Communication dans un congrès
ESOP 2015, Apr 2015, London, United Kingdom. Lecture Notes in Computer Science, 2015, Programming Languages and Systems - 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings. 〈10.1007/978-3-662-46669-8_15〉
Liste complète des métadonnées

Littérature citée [38 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01212587
Contributeur : Jasmin Christian Blanchette <>
Soumis le : mercredi 7 octobre 2015 - 15:27:01
Dernière modification le : lundi 20 novembre 2017 - 15:14:02
Document(s) archivé(s) le : vendredi 8 janvier 2016 - 10:15:52

Fichier

wit.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel. Witnessing (Co)datatypes. ESOP 2015, Apr 2015, London, United Kingdom. Lecture Notes in Computer Science, 2015, Programming Languages and Systems - 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings. 〈10.1007/978-3-662-46669-8_15〉. 〈hal-01212587〉

Partager

Métriques

Consultations de la notice

109

Téléchargements de fichiers

52