Type Systems for Information Flow Control

Functional type systems

Heintze and Riecke @ POPL 1998 present the SLam Calculus.
Abadi et al. @ POPL 1999 present a foundational type system, the Dependency Core Calculus (DCC). They prove the noninterference property (NI) through a denotational model, later called classified sets. They then infer the NI for a series of other calculi by embedding them in the DCC.

References

Heintze, Nevin, and Jon G. Riecke. 1998. ‘The SLam Calculus: Programming with Secrecy and Integrity’. In Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 365–77. Association for Computing Machinery. https://doi.org/10.1145/268946.268976. pdf

@inproceedings{heintze_1998,
	title = {The {SLam} calculus: programming with secrecy and integrity},
	doi = {10.1145/268946.268976},
	booktitle = {Proceedings of the 25th {ACM} {SIGPLAN}-{SIGACT} {Symposium} on {Principles} of {Programming} {Languages}},
	publisher = {Association for Computing Machinery},
	author = {Heintze, Nevin and Riecke, Jon G.},
	year = {1998},
	pages = {365--377}
}

Abadi, Martín, Anindya Banerjee, Nevin Heintze, and Jon G Riecke. 1999. ‘A Core Calculus of Dependency’. In Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 147–60. Association for Computing Machinery. https://doi.org/10.1145/292540.292555. pdf

@inproceedings{abadi_1999,
	title = {A core calculus of dependency},
	doi = {10.1145/292540.292555},
	booktitle = {Proceedings of the 26th {ACM} {SIGPLAN}-{SIGACT} {Symposium} on {Principles} of {Programming} {Languages}},
	publisher = {Association for Computing Machinery},
	author = {Abadi, Mart\acute{i}n and Banerjee, Anindya and Heintze, Nevin and Riecke, Jon G},
	year = {1999},
	pages = {147--160}
}