K. Asai and Y. Kameyama, Polymorphic Delimited Continuations, Proceedings of the 5th Asian Symposium on Programming Languages and Systems (APLAS'07), pp.239-254, 2007.
DOI : 10.1007/978-3-540-76637-7_16
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.106.9907

V. Balat, R. D. Cosmo, and M. P. Fiore, Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums, Proceedings of the Thirty-First Annual ACM Symposium on Principles of Programming Languages, pp.64-76, 2004.
DOI : 10.1145/982962.964007
URL : https://hal.archives-ouvertes.fr/hal-00149561

N. Benton and V. Koutavas, A mechanized bisimulation for the nu-calculus, 2008.

M. Biernacka, D. Biernacki, and O. Danvy, An operational foundation for delimited continuations in the CPS hierarchy, Logical Methods in Computer Science, vol.1, issue.25, pp.1-39, 2005.

D. Biernacki and O. Danvy, THEORETICAL PEARL: A simple proof of a folklore theorem about delimited control, Journal of Functional Programming, vol.16, issue.03, pp.269-280, 2006.
DOI : 10.1017/S0956796805005782

D. Biernacki and S. Lenglet, Applicative Bisimulations for Delimited-Control Operators, Foundations of Software Science and Computation Structures, 15th International Conference (FOSSACS'12), pp.119-134, 2012.
DOI : 10.1007/978-3-642-28729-9_8
URL : https://hal.archives-ouvertes.fr/hal-01399945

D. Biernacki and S. Lenglet, Normal Form Bisimulations for Delimited-Control Operators, Functional and Logic Programming, 13th International Symposium (FLOPS'12), pp.47-61, 2012.
DOI : 10.1007/978-3-642-29822-6_7
URL : https://hal.archives-ouvertes.fr/hal-01399951

D. Biernacki and S. Lenglet, Environmental Bisimulations for Delimited-Control Operators, Proceedings of the 11th Asian Symposium on Programming Languages and Systems (APLAS'13), pp.333-348, 2013.
DOI : 10.1007/978-3-319-03542-0_24
URL : https://hal.archives-ouvertes.fr/hal-00903839

D. Biernacki, S. Lenglet, and P. Polesiuk, Bisimulations for delimited-control operators Avalaible at https://hal.inria.fr/hal-01207112, 2015.
DOI : 10.1007/978-3-642-28729-9_8
URL : http://arxiv.org/abs/1201.0874

D. Biernacki and P. Polesiuk, Logical relations for coherence of effect subtyping, Typed Lambda Calculi and Applications, 13th International Conference of Leibniz International Proceedings in Informatics, pp.107-122, 2015.

P. Curien and H. Herbelin, The duality of computation, Proceedings of the 2000 ACM SIGPLAN International Conference on Functional Programming (ICFP'00), pp.233-243, 2000.
URL : https://hal.archives-ouvertes.fr/inria-00156377

O. Danvy and A. Filinski, Abstracting control, Proceedings of the 1990 ACM conference on LISP and functional programming , LFP '90, pp.151-160, 1990.
DOI : 10.1145/91556.91622

D. Dreyer, G. Neis, and L. Birkedal, The impact of higher-order state and control effects on local relational reasoning, Journal of Functional Programming, vol.69, issue.4-5, pp.477-528, 2012.
DOI : 10.1145/1889997.1890002

R. , K. Dybvig, S. Peyton-jones, and A. Sabry, A monadic framework for delimited continuations, Journal of Functional Programming, vol.17, issue.6, pp.687-730, 2007.

M. Felleisen, The theory and practice of first-class prompts, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '88, pp.180-190, 1988.
DOI : 10.1145/73560.73576

A. Filinski, Declarative continuations: An investigation of duality in programming language semantics, Category Theory and Computer Science, number 389 in Lecture Notes in Computer Science, pp.224-249, 1989.
DOI : 10.1007/BFb0018355

A. Filinski, Representing monads, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '94, pp.446-457, 1994.
DOI : 10.1145/174675.178047

M. Flatt, G. Yu, R. B. Findler, and M. Felleisen, Adding delimited and composable control to a production programming environment, Proceedings of the 2007 ACM SIGPLAN International Conference on Functional Programming (ICFP'07), pp.165-176, 2007.
DOI : 10.1145/1291220.1291178
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.63.2126

C. Gunter, D. Rémy, and J. G. Riecke, A generalization of exceptions and control in ML-like languages, Proceedings of the seventh international conference on Functional programming languages and computer architecture , FPCA '95, pp.12-23, 1995.
DOI : 10.1145/224164.224173

C. Hur, D. Dreyer, G. Neis, and V. Vafeiadis, The marriage of bisimulations and Kripke logical relations, Proceedings of the Thirty-Ninth Annual ACM Symposium on Principles of Programming Languages, pp.59-72, 2012.

C. Hur, G. Neis, D. Dreyer, and V. Vafeiadis, A logical step forward in parametric bisimulations, Max Planck Institute for Software Systems (MPI- SWS), 2014.

Y. Kameyama, Axioms for control operators in the CPS hierarchy. Higher-Order and Symbolic Computation, pp.339-369, 2007.

Y. Kameyama and M. Hasegawa, A sound and complete axiomatization of delimited continuations, Shivers [35], pp.177-188

O. Kiselyov, Delimited Control in OCaml, Abstractly and Concretely: System Description, Functional and Logic Programming, 10th International Symposium, FLOPS 2010, pp.304-320, 2010.
DOI : 10.1007/978-3-642-12251-4_22
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.183.3363

I. Kobori, Y. Kameyama, and O. Kiselyov, ATM without tears: prompt-passing style transformation for typed delimited-control operators, 2015 Workshop on Continuations: Pre-proceedings, 2015.
DOI : 10.4204/eptcs.212.3
URL : http://arxiv.org/abs/1606.06379

V. Koutavas, P. B. Levy, and E. Sumii, From Applicative to Environmental Bisimulation, Proceedings of the 27th Annual Conference on Mathematical Foundations of Programming Semantics (MFPS XXVII), pp.215-235, 2011.
DOI : 10.1016/j.entcs.2011.09.023
URL : http://doi.org/10.1016/j.entcs.2011.09.023

V. Koutavas and M. Wand, Bisimulations for Untyped Imperative Objects, 15th European Symposium on Programming, pp.146-161, 2006.
DOI : 10.1006/inco.1995.1018

V. Koutavas and M. Wand, Small bisimulations for reasoning about higher-order imperative programs, Proceedings of the 33rd Annual ACM Symposium on Principles of Programming Languages, pp.141-152, 2006.
DOI : 10.1145/1111320.1111050

J. Madiot, Higher-Order Languages: Dualities and Bisimulation Enhancements, 2015.
URL : https://hal.archives-ouvertes.fr/tel-01141067

J. Madiot, D. Pous, and D. Sangiorgi, Bisimulations Up-to: Beyond First-Order Transition Systems, 25th International Conference on Concurrency Theory, pp.93-108, 2014.
DOI : 10.1007/978-3-662-44584-6_8
URL : https://hal.archives-ouvertes.fr/hal-00990859

A. Piérard and E. Sumii, A Higher-Order Distributed Calculus with Name Creation, 2012 27th Annual IEEE Symposium on Logic in Computer Science, pp.531-540, 2012.
DOI : 10.1109/LICS.2012.63

A. Pitts and I. Stark, Operational reasoning for functions with local state, Higher Order Operational Techniques in Semantics, pp.227-273, 1998.

D. Pous and D. Sangiorgi, Enhancements of the bisimulation proof method, Advanced Topics in Bisimulation and Coinduction, pp.233-289, 2011.
DOI : 10.1017/CBO9780511792588.007
URL : https://hal.archives-ouvertes.fr/hal-00909391

D. Sangiorgi, N. Kobayashi, and E. Sumii, Environmental bisimulations for higher-order languages, ACM Transactions on Programming Languages and Systems, vol.33, issue.1, pp.1-69, 2011.
DOI : 10.1145/1889997.1890002
URL : https://hal.archives-ouvertes.fr/hal-01337665

E. Sumii, A Complete Characterization of Observational Equivalence in Polymorphic ??-Calculus with General References, Computer Science Logic, CSL'09, pp.455-469, 2009.
DOI : 10.1109/LICS.2007.21

E. Sumii and B. C. Pierce, A bisimulation for dynamic sealing, Theoretical Computer Science, vol.375, issue.1-3, pp.169-192, 2007.
DOI : 10.1016/j.tcs.2006.12.032
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.103.867

E. Sumii and B. C. Pierce, A bisimulation for type abstraction and recursion, Journal of the ACM, vol.54, issue.5, 2007.
DOI : 10.1145/1040305.1040311
URL : http://basics.sjtu.edu.cn/~yuehg/popl/a bisimulation for type abstraction and recursion (2005).pdf

P. Wadler, Call-by-value is dual to call-by-name, Shivers [35], pp.189-201
DOI : 10.1145/944705.944723

T. Yachi and E. Sumii, A Sound and Complete Bisimulation for Contextual Equivalence in $$\lambda $$ -Calculus with Call/cc, Proceedings of the 14th Asian Symposium on Programming Languages and Systems (APLAS'16), pp.171-186, 2016.
DOI : 10.1145/1047659.1040311