More Web Proxy on the site http://driver.im/

Article

Translating dependency into parametricity

Authors:

Steve ZdancewicAuthors Info & Claims

ICFP '04: Proceedings of the ninth ACM SIGPLAN international conference on Functional programming

Pages 115 - 125

https://doi.org/10.1145/1016850.1016868

Published: 19 September 2004 Publication History

Abstract

Abadi et al. introduced the dependency core calculus (DCC) as a unifying framework to study many important program analyses such as binding time, information flow, slicing, and function call tracking. DCC uses a lattice of monads and a nonstandard typing rule for their associated bind operations to describe the dependency of computations in a program. Abadi et al. proved a noninterference theorem that establishes the correctness of DCC's type system and thus the correctness of the type systems for the analyses above.In this paper, we study the relationship between DCC and the Girard-Reynolds polymorphic lambda calculus (System F). We encode the recursion-free fragment of DCC into F via a type-directed translation. Our main theoretical result is that, following from the correctness of the translation, the parametricity theorem for F implies the noninterference theorem for DCC. In addition, the translation provides insights into DCC's type system and suggests implementation strategies of dependency calculi in polymorphic languages.

References

[1]

Martín Abadi, Anindya Banerjee, Nevin Heintze, and Jon Riecke. A core calculus of dependency. In Proc. 26th ACM Symp. on Principles of Programming Languages (POPL), pages 147--160, San Antonio, TX, January 1999.]]

Digital Library

[2]

Nick Benton. Simple relational correctness proofs for static analyses and program transformations. In Proc. 31st ACM Symp. on Principles of Programming Languages (POPL), pages 14--25. ACM Press, 2004.]]

Digital Library

[3]

Matthew Fluet and Greg Morrisett. Monadic regions. In Proc. ACM SIGPLAN International Conference on Functional Programming (ICFP), 2004.]]

Digital Library

[4]

Matthew Fluet and Riccardo Pucella. Phantom types and subtyping. In Proc. of the 2nd IFIP International Conference on Theoretical Computer Science, 2002.]]

Digital Library

[5]

J.-Y. Girard. Interprétation Functionelle et Élimination des Coupures dans l'Arithmétique d'Order Supérieure. PhD thesis, Université Paris VII, 1972.]]

[6]

Nevin Heintze and Jon G. Riecke. The SLam calculus: Programming with secrecy and integrity. In Proc. 25th ACM Symp. on Principles of Programming Languages (POPL), San Diego, California, 1998.]]

Digital Library

[7]

Patricia Johann and Janis Voigtländer. Free theorems in the presence of seq. In Proc. 31st ACM Symp. on Principles of Programming Languages (POPL), 2004.]]

Digital Library

[8]

J. Launchbury and R. Paterson. Parametricity and unboxing with pointed types. In Proc. of the 9th European Symposium on Programming, 1996.]]

Digital Library

[9]

John C. Mitchell. Foundations for Programming Languages. The MIT Press, 1996.]]

Digital Library

[10]

Eugenio Moggi. Notions of computation and monads. Information and Computation, 1:55--92, 1991.]]

Digital Library

[11]

Benjamin C. Pierce. Types and Programming Languages. The MIT Press, 2002.]]

Digital Library

[12]

François Pottier and Vincent Simonet. Information flow inference for ML. In Proc. 29th ACM Symp. on Principles of Programming Languages (POPL), 2002.]]

Digital Library

[13]

John C. Reynolds. Towards a theory of type structure. In Programming Symposium, volume 19 of Lecture Notes in Computer Science. Springer-Verlag, 1974.]]

Digital Library

[14]

John C. Reynolds. Types, abstraction, and parametric polymorphism. In Information Processing. Elsevier Science Publishers B.V., 1983.]]

[15]

Andrei Sabelfeld and Andrew C. Myers. Language-based information-flow security. IEEE Journal on Selected Areas in Communications, 21(1):5--19, January 2003.]]

Digital Library

[16]

Andrei Sabelfeld and David Sands. A PER model of secure information flow in sequential programs. Higher-Order and Symbolic Computation, 14(1):59--91, March 2001.]]

Digital Library

[17]

Eijiro Sumii and Benjamin C. Pierce. Logical relations for encryption. In Proc. of the 14th IEEE Computer Security Foundations Workshop, 2001.]]

[18]

Eijiro Sumii and Benjamin C. Pierce. A bisimulation for dynamic sealing. In Proc. 31st ACM Symp. on Principles of Programming Languages (POPL). ACM Press, 2004.]]

Digital Library

[19]

Stephen Tse and Steve Zdancewic. Run-time principals in information-flow type systems. In Proc. IEEE Symposium on Security and Privacy, 2004. To Appear.]]

[20]

Stephen Tse and Steve Zdancewic. Translating dependency into parametricity. Technical report, University of Pennsylvania, January 2004.]]

[21]

Dennis Volpano, Geoffrey Smith, and Cynthia Irvine. A sound type system for secure flow analysis. Journal of Computer Security, 4(3):167--187, 1996.]]

Digital Library

[22]

Philip Wadler. Theorems for free! In Proceedings of the 4th International Symposium on Functional Programming and Computer Architecture, September 1989.]]

Digital Library

[23]

Geoffrey Washburn and Stephanie Weirich. Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism. In Proc. of the 8th ACM SIGPLAN International Conference on Functional Programming, Upsala, Sweden, August 2003.]]

Digital Library

[24]

Stephan Zdancewic. Programming Languages for Information Security. PhD thesis, Cornell University, 2002.]]

Digital Library

[25]

Steve Zdancewic and Andrew C. Myers. Secure information flow and CPS. In Proc. of the 10th European Symposium on Programming, 2001.]]

Digital Library

Cited By

Gollamudi AChong SRanise SCarbone RTakabi D(2023)Expressive Authorization Policies using Computation PrincipalsProceedings of the 28th ACM Symposium on Access Control Models and Technologies10.1145/3589608.3593834(107-119)Online publication date: 24-May-2023
https://dl.acm.org/doi/10.1145/3589608.3593834
Choudhury P(2022)Monadic and comonadic aspects of dependency analysisProceedings of the ACM on Programming Languages10.1145/35633356:OOPSLA2(1320-1348)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563335
Hirsch ACecchetti E(2021)Giving semantics to program-counter labels via secure effectsProceedings of the ACM on Programming Languages10.1145/34343165:POPL(1-29)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434316
Show More Cited By

Index Terms

Translating dependency into parametricity
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages

Recommendations

Translating dependency into parametricity
ICFP '04

Abadi et al. introduced the dependency core calculus (DCC) as a unifying framework to study many important program analyses such as binding time, information flow, slicing, and function call tracking. DCC uses a lattice of monads and a nonstandard ...
Noninterference for free
ICFP 2015: Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming

The dependency core calculus (DCC) is a framework for studying a variety of dependency analyses (e.g., secure information flow). The key property provided by DCC is noninterference, which guarantees that a low-level observer (attacker) cannot ...
Noninterference for free
ICFP '15

The dependency core calculus (DCC) is a framework for studying a variety of dependency analyses (e.g., secure information flow). The key property provided by DCC is noninterference, which guarantees that a low-level observer (attacker) cannot ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICFP '04: Proceedings of the ninth ACM SIGPLAN international conference on Functional programming

September 2004

264 pages

ISBN:1581139055

DOI:10.1145/1016850

General Chair:
Chris Okasaki
United States Military Academy, West Point
,
Program Chair:
Kathleen Fisher
AT&T Labs Research

ACM SIGPLAN Notices Volume 39, Issue 9
ICFP '04
September 2004
254 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1016848
Issue’s Table of Contents

Copyright © 2004 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 19 September 2004

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

ICFP04

Sponsor:

ICFP04: ACM SIGPLAN International Conference on Functional Programming

September 19 - 21, 2004

UT, Snow Bird, USA

Acceptance Rates

Overall Acceptance Rate 333 of 1,064 submissions, 31%

Upcoming Conference

ICFP '25

Sponsor:
sigplan

ACM SIGPLAN International Conference on Functional Programming

October 12 - 18, 2025

Singapore , Singapore

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

67
Total Citations
View Citations
384
Total Downloads

Downloads (Last 12 months)5
Downloads (Last 6 weeks)1

Reflects downloads up to 11 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Gollamudi AChong SRanise SCarbone RTakabi D(2023)Expressive Authorization Policies using Computation PrincipalsProceedings of the 28th ACM Symposium on Access Control Models and Technologies10.1145/3589608.3593834(107-119)Online publication date: 24-May-2023
https://dl.acm.org/doi/10.1145/3589608.3593834
Choudhury P(2022)Monadic and comonadic aspects of dependency analysisProceedings of the ACM on Programming Languages10.1145/35633356:OOPSLA2(1320-1348)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563335
Hirsch ACecchetti E(2021)Giving semantics to program-counter labels via secure effectsProceedings of the ACM on Programming Languages10.1145/34343165:POPL(1-29)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434316
Gregersen SBay JTimany ABirkedal L(2021)Mechanized logical relations for termination-insensitive noninterferenceProceedings of the ACM on Programming Languages10.1145/34342915:POPL(1-29)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434291
Häner THoefler TTroyer M(2020)Assertion-based optimization of Quantum programsProceedings of the ACM on Programming Languages10.1145/34282014:OOPSLA(1-20)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428201
Abel ABernardy J(2020)A unified view of modalities in type systemsProceedings of the ACM on Programming Languages10.1145/34089724:ICFP(1-28)Online publication date: 3-Aug-2020
https://dl.acm.org/doi/10.1145/3408972
Yu TNahrstedt K(2019)ShoesHackerProceedings of the ACM on Interactive, Mobile, Wearable and Ubiquitous Technologies10.1145/33512783:3(1-29)Online publication date: 9-Sep-2019
https://dl.acm.org/doi/10.1145/3351278
Tomé Cortiñas CValliappan NMardziel PVazou N(2019)Simple Noninterference by NormalizationProceedings of the 14th ACM SIGSAC Workshop on Programming Languages and Analysis for Security10.1145/3338504.3357342(61-72)Online publication date: 15-Nov-2019
https://dl.acm.org/doi/10.1145/3338504.3357342
Kavvos G(2019)Modalities, cohesion, and information flowProceedings of the ACM on Programming Languages10.1145/32903333:POPL(1-29)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290333
Morris JMcKinna J(2019)Abstracting extensible data types: or, rows by any other nameProceedings of the ACM on Programming Languages10.1145/32903253:POPL(1-28)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290325
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents