E. If, S. |=-e:-e, and S. |=, ? and |= s : S and e/s a; k ? r

S. If and . |=, ? and S |= k :: ? and |= s : S and s v k ? r

. Proof, The proof is a simple, but tedious induction on the height of the evaluation derivation (the derivation of e/s a; k ? r for (1); the derivation of s v k ? r for (2)), and case analysis on a and k, respectively. We give the main cases; the remaining cases are similar

S. By, S. |=-k, and . |=, By hypothesis S |= v : ? , the value v is a closure (x, a 0 , e 0 ), and (3) E 0 ?x. a 0 : ? 1 ? ? 2 and (4) S e 0 : E 0 for some E 0 . Since v is a closure, the elimination rule for apply1 closures matches. From (3) and (4), we get S |= apply2(x, a 0 , e 0 , k) :: ? 1 . The expected result follows from induction hypothesis

S. We-have and . |=-e, E and, given the typing rule for References [1] A. W. Appel. Compiling with continuations, 1992.

L. Cardelli, Typeful programming, Formal Description of Programming Concepts, pp.431-507

L. Damas, Type assignment in programming languages, 1985.

B. F. Duba, R. Harper, and D. Macqueen, Typing first-class continuations in ML, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '91, pp.163-173, 1991.
DOI : 10.1145/99583.99608
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.22.1725

M. Felleisen and D. P. Friedman, Control operators , the SECD machine and the ?-calculus, Formal Description of Programming Concepts III, pp.131-141, 1986.

D. K. Gifford and J. M. Lucassen, Integrating functional and imperative programming, Proceedings of the 1986 ACM conference on LISP and functional programming , LFP '86, pp.28-38, 1986.
DOI : 10.1145/319838.319848

R. Harper and M. Lillibridge, ML with callcc is unsound. Message sent to the sml mailing list, 1991.

R. Harper, M. Lillibridge10-]-r, M. Harper, and . Lillibridge, Polymorphic type assignment and CPS conversion Explicit polymorphism and CPS conversion, SIGPLAN Continuations Workshop 20th symposium Principles of Programming Languages, 1992.
DOI : 10.1007/bf01019463
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.141.6828

X. Leroy, The ZINC experiment: an economical implementation of the ML language, 1990.
URL : https://hal.archives-ouvertes.fr/inria-00070049

X. Leroy, Typage polymorphe d'un langage algorithmique Doctoral dissertation, 1992.

X. Leroy and P. Weis, Polymorphic type inference and assignment, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '91, pp.291-302
DOI : 10.1145/99583.99622
URL : https://hal.archives-ouvertes.fr/hal-01499974

R. Milner and M. Tofte, Co-induction in relational semantics, Theoretical Computer Science, vol.87, issue.1, pp.209-220, 1991.
DOI : 10.1016/0304-3975(91)90033-X
URL : http://doi.org/10.1016/0304-3975(91)90033-x

R. Milner, M. Tofte, and R. Harper, The definition of Standard ML, 1990.

J. C. Mitchell, Type Systems for Programming Languages, pp.367-458, 1990.
DOI : 10.1016/B978-0-444-88074-1.50013-5

J. Reynolds, Definitional interpreters for higherorder programming languages, Proceedings of the 25th ACM National Conference, pp.717-740
DOI : 10.1145/800194.805852
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.110.5892

J. Talpin and P. Jouvelot, The type and effect discipline, Logic in Computer Science, 1992.
DOI : 10.1109/lics.1992.185530
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.54.5309

M. Tofte, Type inference for polymorphic references . Information and Computation, 1990.
DOI : 10.1016/0890-5401(90)90018-d
URL : http://doi.org/10.1016/0890-5401(90)90018-d

A. K. Wright, Typing references by effect inference, European Symposium on Programming, 1992.
DOI : 10.1007/3-540-55253-7_28
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.15.9668

A. K. Wright and M. Felleisen, A Syntactic Approach to Type Soundness, Information and Computation, vol.115, issue.1, 1991.
DOI : 10.1006/inco.1994.1093
URL : http://doi.org/10.1006/inco.1994.1093