Proving termination of evaluation for System F with control operators

Małgorzata Biernacka 1 Dariusz Biernacki 1 Sergueï Lenglet 2 Marek Materzok 1
1 Faculty of Mathematics and Computer Science [Wroclaw]
2 PAREO - Formal islands: foundations and applications
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : We present new proofs of termination of evaluation in reduction semantics (i.e., a small-step operational semantics with explicit representation of evaluation contexts) for System F with control operators. We introduce a modified version of Girard's proof method based on reducibility candidates, where the reducibility predicates are defined on values and on evaluation contexts as prescribed by the reduction semantics format. We address both abortive control operators (callcc) and delimited-control operators (shift and reset) for which we introduce novel polymorphic type systems, and we consider both the call-by-value and call-by-name evaluation strategies.
Type de document :
Communication dans un congrès
de'Liquoro, Ugo and Saurin, Alexis. COS 2013 - First Workshop on Control Operators and their Semantics, Jun 2013, Eindhoven, Netherlands. Open Publishing Association, 127, pp.15-29, 2013, Electronic Proceedings in Theoretical Computer Science. 〈10.4204/EPTCS.127.2〉
Liste complète des métadonnées
https://hal.inria.fr/hal-00860954
Contributeur : Sergueï Lenglet <>
Soumis le : mercredi 11 septembre 2013 - 15:10:51
Dernière modification le : mardi 23 janvier 2018 - 15:14:11

Lien texte intégral

arxiv

Identifiants

Collections

INRIA | UNIV-LORRAINE | LORIA-FM | LORIA

Citation

Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, Marek Materzok. Proving termination of evaluation for System F with control operators. de'Liquoro, Ugo and Saurin, Alexis. COS 2013 - First Workshop on Control Operators and their Semantics, Jun 2013, Eindhoven, Netherlands. Open Publishing Association, 127, pp.15-29, 2013, Electronic Proceedings in Theoretical Computer Science. 〈10.4204/EPTCS.127.2〉. 〈hal-00860954〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

173

Contact


archive-ouverte@inria.fr