[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.
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}
}