Witnessing (co)datatypes

Conference paper

Blanchette, J., Popescu, A. and Traytel, D. 2015. Witnessing (co)datatypes. 24th European Symposium on Programming (ESOP 2015). London, UK 11 - 18 Apr 2015 Springer. pp. 359-382
TypeConference paper
TitleWitnessing (co)datatypes
AuthorsBlanchette, J., Popescu, A. and Traytel, D.
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.

Research GroupFoundations of Computing group
Conference24th European Symposium on Programming (ESOP 2015)
Page range359-382
ISSN0302-9743
ISBN
Hardcover9783662466681
PublisherSpringer
Publication dates
Print2015
Publication process dates
Deposited27 Apr 2015
Output statusPublished
Accepted author manuscript
Copyright Statement

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-662-46669-8_15

Additional information

Published paper appears in: Programming Languages and Systems, Volume 9032 of the series Lecture Notes in Computer Science pp 359-382, 2015

Web address (URL)http://dx.doi.org/10.1007/978-3-662-46669-8_15
LanguageEnglish
Book titleProgramming languages and systems : 24th European Symposium on Programming, ESOP 2015, held as art of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings
Permalink -

https://repository.mdx.ac.uk/item/851zx

Log in to edit

Download files

Accepted author manuscript
ESOP2015.pdf

  • 27
    total views
  • 5
    total downloads
  • 1
    views this month
  • 1
    downloads this month

Export as