The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

alexandre p wrote:
> I like how your naïve IO allows one to prove things about the input 
> and output
> streams by exposing some of the plumbing, but the obvious downside is
> that such a scheme would quickly become too unwieldy to extend.
>
> Has anyone thought about how to deal with I/O in a dependently typed
> environment?
>    

The Ynot library might qualify:
    http://ynot.cs.harvard.edu/