PLS Lab

The CK machine

The CK machine is an abstract machine that supports a number of evaluation strategies, including call-by-name and call-by-value evaluation.

It was introduced in Felleisen and Friedman 1987 as a simplification of Landin's SECD machine Levy 2003, 2.3.2.

A more modern version of the CK machine plays a central role in the study of call-by-push-value Levy 2003.

Description

Please expand.

See also

Similar machines:

References

Felleisen, Matthias, and D.P. Friedman. 1987. ‘Control Operators, the SED-Machine, and the λ-Calculus’. In Formal Description of Programming Concepts III, edited by Martin Wirsing. North-Holland. pdf. 
@inproceedings{felleisen_1987,
	title = {Control operators, the {SED}-machine, and the λ-calculus},
	isbn = {978-0-444-70253-1},
	url = {https://legacy.cs.indiana.edu/ftp/techreports/TR197.pdf},
	booktitle = {Formal {Description} of {Programming} {Concepts} {III}},
	publisher = {North-Holland},
	author = {Felleisen, Matthias and Friedman, D.P.},
	editor = {Wirsing, Martin},
	year = {1987},
}
Levy, Paul Blain. 2003. Call-by-Push-Value: A Functional-Imperative Synthesis. Semantic Structures in Computation. Springer Dordrecht. https://doi.org/10.1007/978-94-007-0954-6. 
@book{levy_2003,
	series = {Semantic {Structures} in {Computation}},
	title = {Call-by-{Push}-{Value}: {A} {Functional}-{Imperative} {Synthesis}},
	isbn = {978-94-010-3752-5},
	publisher = {Springer Dordrecht},
	author = {Levy, Paul Blain},
	year = {2003},
	doi = {10.1007/978-94-007-0954-6},
}
Bierman, G. M. 1998. ‘A Computational Interpretation of the Λμ-Calculus’. In Mathematical Foundations of Computer Science 1998, edited by Luboš Brim, Jozef Gruska, and Jiří Zlatuška, 1450:336–45. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer Berlin Heidelberg. https://doi.org/10.1007/BFb0055783. 
@inproceedings{bierman_1998,
	address = {Berlin, Heidelberg},
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {A computational interpretation of the λμ-calculus},
	volume = {1450},
	url = {http://link.springer.com/10.1007/BFb0055783},
	doi = {10.1007/BFb0055783},
	urldate = {2023-05-10},
	booktitle = {Mathematical {Foundations} of {Computer} {Science} 1998},
	publisher = {Springer Berlin Heidelberg},
	author = {Bierman, G. M.},
	editor = {Brim, Luboš and Gruska, Jozef and Zlatuška, Jiří},
	year = {1998},
	pages = {336--345},
}
Streicher, Th., and B. Reus. 1998. ‘Classical Logic, Continuation Semantics and Abstract Machines’. Journal of Functional Programming 8 (6): 543–72. https://doi.org/10.1017/S0956796898003141. 
@article{streicher_1998,
	title = {Classical logic, continuation semantics and abstract machines},
	volume = {8},
	doi = {10.1017/S0956796898003141},
	number = {6},
	journal = {Journal of Functional Programming},
	author = {Streicher, Th. and Reus, B.},
	year = {1998},
	pages = {543--572},
}