The Coq mailing list

[Conor McBride <ctm AT cs.nott.ac.uk>]

Hi folks

Pierre Casteran wrote:

> Well, There is some stuff about that pp 389-390, and more examples in 
> the Tutorial on [co-]inductive
> types (reachable from Coq's documentation page : look at  "Additional 
> Documentation").
>
> Speaking about I/O, there is probably some interesting work [to be ?] 
> done using co-inductive types for
> representing I/O streams, but I don't have any precise links.


A few people have given some thought to I/O in type theory, most notably 
Peter Hancock, Anton Setzer and Pierre Hyvernat. For useful reading, try

 http://homepages.inf.ed.ac.uk/v1phanc1/chat.html

All the best

Conor

This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.