Effect systems

Effect systems (also called type-and-effect systems) are a kind of type system that also tracks the effects that a program may perform. They usually compute upper bounds, i.e. conservative approximations that overestimate which effects may be performed.

Effect systems were introduced by Gifford and Lucassen in the late 1980s.

References

The first paper on effect systems appears to have been at LFP 1986:

Gifford, David K., and John M. Lucassen. 1986. ‘Integrating Functional and Imperative Programming’. In Proceedings of the 1986 ACM Conference on LISP and Functional Programming - LFP ’86, 28–38. Association for Computing Machinery. https://doi.org/10.1145/319838.319848.

@inproceedings{gifford_1986,
	title = {Integrating functional and imperative programming},
	doi = {10.1145/319838.319848},
	pages = {28--38},
	booktitle = {Proceedings of the 1986 {ACM} conference on {LISP} and Functional Programming - {LFP} '86},
	publisher = {Association for Computing Machinery},
	author = {Gifford, David K. and Lucassen, John M.},
	date = {1986}
}

This paper was quickly followed by one at POPL 1988, which added polymorphism:

Lucassen, John M., and David K. Gifford. 1988. ‘Polymorphic Effect Systems’. In Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - POPL ’88, 47–57. Association for Computing Machinery. https://doi.org/10.1145/73560.73564.

@inproceedings{lucassen_1988,
	title = {Polymorphic effect systems},
	doi = {10.1145/73560.73564},
	pages = {47--57},
	booktitle = {Proceedings of the 15th {ACM} {SIGPLAN}-{SIGACT} symposium on Principles of Programming Languages  - {POPL} '88},
	publisher = {Association for Computing Machinery},
	author = {Lucassen, John M. and Gifford, David K.},
	date = {1988},
}

A survey of the state-of-the-art in 1999 can be found in

Nielson, Flemming, and Hanne Riis Nielson. 1999. ‘Type and Effect Systems’. In Correct System Design, edited by Ernst-Rüdiger Olderog and Bernhard Steffen, 114–36. Lecture Notes in Computer Science 1710. Berlin, Heidelberg: Springer Berlin Heidelberg. https://doi.org/10.1007/3-540-48092-7_6. pdf

@incollection{nielson_1999,
	location = {Berlin, Heidelberg},
	title = {Type and Effect Systems},
	series = {Lecture Notes in Computer Science},
	pages = {114--136},
	number = {1710},
	booktitle = {Correct System Design},
	publisher = {Springer Berlin Heidelberg},
	author = {Nielson, Flemming and Nielson, Hanne Riis},
	editor = {Olderog, Ernst-Rüdiger and Steffen, Bernhard},
	date = {1999},
	doi = {10.1007/3-540-48092-7_6}
}