|
 
|
[Cro15b] A verified abstract machine for functional coroutine (companion technical report)
Rapport Scientifique : Date de dépot: 2015/04/12, Nb pages 11, (Tech. Rep.: CEDRIC-15-3514)
motcle:
Résumé:
Functional coroutines are a restricted form of control mechanism, where each continuation comes with its local environment. This restriction was originally obtained by considering a constructive version of Parigot's classical natural deduction which is sound and complete for the Constant Domain logic. In this article, we present a reï¬nement of de Groote's abstract machine which is proved to be correct for functional coroutines. Therefore, this abstract machine also provides a direct computational interpretation of the Constant Domain logic.
BibTeX
| @techreport { | |||
| Cro15b, | |||
| title | = | "{A verified abstract machine for functional coroutine (companion technical report)}", | |
| author | = | "T. Crolard", | |
| number | = | "{CEDRIC-15-3514}", | |
| institution | = | "{CEDRIC laboratory, CNAM-Paris, France}", | |
| date | = | {12-04-2015}, | |
| pages | = | "11", | |
| } | |||
