{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:31:18Z","timestamp":1774837878135,"version":"3.50.1"},"reference-count":21,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2019,7,26]],"date-time":"2019-07-26T00:00:00Z","timestamp":1564099200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,7,26]]},"abstract":"<jats:p>In this paper we revisit the connection between parametricity and noninterference. Our primary contribution is a proof of noninterference for a polyvariant variation of the Dependency Core Calculus of in the Calculus of Constructions. The proof is modular: it leverages parametricity for the Calculus of Constructions and the encoding of data abstraction using existential types. This perspective gives rise to simple and understandable proofs of noninterference from parametricity. All our contributions have been mechanised in the Agda proof assistant.<\/jats:p>","DOI":"10.1145\/3341693","type":"journal-article","created":{"date-parts":[[2019,7,29]],"date-time":"2019-07-29T20:55:51Z","timestamp":1564433751000},"page":"1-22","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["Simple noninterference from parametricity"],"prefix":"10.1145","volume":"3","author":[{"given":"Maximilian","family":"Algehed","sequence":"first","affiliation":[{"name":"Chalmers University of Technology, Sweden"}]},{"given":"Jean-Philippe","family":"Bernardy","sequence":"additional","affiliation":[{"name":"University of Gothenburg, Sweden"}]}],"member":"320","published-online":{"date-parts":[[2019,7,26]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292555"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110265"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3264820.3264823"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3139337.3139338"},{"key":"e_1_2_2_5_1","volume-title":"Lambda calculus with types","author":"Barendregt Henk","unstructured":"Henk Barendregt , Wil Dekkers , and Richard Statman . 2013. Lambda calculus with types . Cambridge University Press . Henk Barendregt, Wil Dekkers, and Richard Statman. 2013. Lambda calculus with types. Cambridge University Press."},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796812000056"},{"key":"e_1_2_2_7_1","volume-title":"Interactive theorem proving and program development: Coq\u2019Art: the calculus of inductive constructions","author":"Bertot Yves","unstructured":"Yves Bertot and Pierre Cast\u00e9ran . 2013. Interactive theorem proving and program development: Coq\u2019Art: the calculus of inductive constructions . Springer Science & amp; Business Media. Yves Bertot and Pierre Cast\u00e9ran. 2013. Interactive theorem proving and program development: Coq\u2019Art: the calculus of inductive constructions. Springer Science &amp; Business Media."},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784733"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784758"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/6041.6042"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_2_2_14_1","unstructured":"John C Reynolds. 1983. Types abstraction and parametric polymorphism. (1983).  John C Reynolds. 1983. Types abstraction and parametric polymorphism. (1983)."},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784756"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1543134.1411289"},{"key":"e_1_2_2_17_1","volume-title":"Proving Noninterference by a Fully Complete Translation to the Simply Typed lambda-calculus. CoRR abs\/0808.3307","author":"Shikuma Naokata","year":"2008","unstructured":"Naokata Shikuma and Atsushi Igarashi . 2008. Proving Noninterference by a Fully Complete Translation to the Simply Typed lambda-calculus. CoRR abs\/0808.3307 ( 2008 ). arXiv: 0808.3307 http:\/\/arxiv.org\/abs\/0808.3307 Naokata Shikuma and Atsushi Igarashi. 2008. Proving Noninterference by a Fully Complete Translation to the Simply Typed lambda-calculus. CoRR abs\/0808.3307 (2008). arXiv: 0808.3307 http:\/\/arxiv.org\/abs\/0808.3307"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2096148.2034688"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1016848.1016868"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2993600.2993608"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2017.12.003"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/99370.99404"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3341693","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3341693","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:41:30Z","timestamp":1750200090000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3341693"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,7,26]]},"references-count":21,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2019,7,26]]}},"alternative-id":["10.1145\/3341693"],"URL":"https:\/\/doi.org\/10.1145\/3341693","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,7,26]]},"assertion":[{"value":"2019-07-26","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}