Skip to Main content Skip to Navigation
Conference papers

Proving termination of evaluation for System F with control operators

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.
Complete list of metadata
Contributor : Sergueï Lenglet Connect in order to contact the contributor
Submitted on : Wednesday, September 11, 2013 - 3:10:51 PM
Last modification on : Saturday, June 25, 2022 - 7:43:11 PM

Links full text




Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, Marek Materzok. Proving termination of evaluation for System F with control operators. COS 2013 - First Workshop on Control Operators and their Semantics, Jun 2013, Eindhoven, Netherlands. pp.15-29, ⟨10.4204/EPTCS.127.2⟩. ⟨hal-00860954⟩



Record views