| HAL-Inria | Publications, software ... of Inria's scientists |
Conference papers
A continuation-passing-style interpretation of simply-typed call-by-need λ-calculus with control within System F
Abstract : Ariola et al defined a call-by-need λ-calculi with control, together with a sequent calculus presentation of it, and a mechanically generated continuation-passing-style transformation simulating the reduction. We present here a simply-typed version of this calculus and shows that it maps to System F through the continuation-passing-style transformation. This implies in particular the normaliza-tion of this simply-typed call-by-need calculus with control. Incidentally, we treat bound variables for the continuation-passing-style transformation in a precise way using indices rather than up to α-conversion, what makes it directly implementable.
Cited literature [15 references]
https://hal.inria.fr/hal-01302696
Contributor : Étienne Miquey <>
Submitted on : Wednesday, May 25, 2016 - 6:53:49 PM
Last modification on : Friday, April 10, 2020 - 5:08:54 PM
Contributor : Étienne Miquey <>
Submitted on : Wednesday, May 25, 2016 - 6:53:49 PM
Last modification on : Friday, April 10, 2020 - 5:08:54 PM
File
cbncps.pdf
Files produced by the author(s)
Licence
Distributed under a Creative Commons Attribution 4.0 International License