Computational \lambda-calculus

The computational \lambda-calculus (\lambda_c) is a calculus designed to model a small functional programming language equipped with effects. It was introduced by Eugenio Moggi in 1989.

Because of the difficult interaction of effects with call-by-name, the computational \lambda-calculus is a call-by-value calculus.

\lambda_c is one of many alternative proposals for an effectful \lambda-calculus (others include fine grain CBV and CBPV).

References

The computational \lambda-calculus was introduced in a LICS 1989 paper by Eugenio Moggi:

E. Moggi, "Computational lambda-calculus and monads," 1989 Proceedings. Fourth Annual Symposium on Logic in Computer Science, Pacific Grove, CA, USA, 1989, pp. 14-23, doi: 10.1109/LICS.1989.39155. pdf

@inproceedings{39155,
  author={Moggi, Eugenio},
  booktitle={[1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science}, 
  title={Computational lambda-calculus and monads}, 
  year={1989},
  pages={14-23},
  doi={10.1109/LICS.1989.39155}
}

A simple operational and denotational semantics for a version of \lambda_c equipped with a large class of algebraic effects is given in

Plotkin, Gordon, and John Power. 2001. ‘Adequacy for Algebraic Effects’. In Foundations of Software Science and Computation Structures, edited by Furio Honsell and Marino Miculan. Vol. 2030. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer Berlin Heidelberg. https://doi.org/10.1007/3-540-45315-6_1. pdf

@inproceedings{plotkin_2001,
	address = {Berlin, Heidelberg},
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {Adequacy for {Algebraic} {Effects}},
	volume = {2030},
	doi = {10.1007/3-540-45315-6_1},
	booktitle = {Foundations of {Software} {Science} and {Computation} {Structures}},
	publisher = {Springer Berlin Heidelberg},
	author = {Plotkin, Gordon and Power, John},
	editor = {Honsell, Furio and Miculan, Marino},
	year = {2001}
}