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

research-article

Open access

Parametricity versus the universal type

Authors:

Dominique Devriese,

Marco Patrignani,

Frank PiessensAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 2, Issue POPL

Article No.: 38, Pages 1 - 23

https://doi.org/10.1145/3158126

Published: 27 December 2017 Publication History

Abstract

There has long been speculation in the scientific literature on how to dynamically enforce parametricity such as that yielded by System F. Almost 20 years ago, Sumii and Pierce proposed a formal compiler from System F into the cryptographic lambda calculus: an untyped lambda calculus extended with an idealised model of encryption. They conjectured that this compiler was fully abstract, i.e. that compiled terms are contextually equivalent if and only if the original terms were, a property that can be seen as a form of secure compilation. The conjecture has received attention in several other publications since then, but remains open to this day.

More recently, several researchers have been looking at gradually-typed languages that extend System F. In this setting it is natural to wonder whether embedding System F into these gradually-typed languages preserves contextual equivalence and thus parametricity.

In this paper, we answer both questions negatively. We provide a concrete counterexample: two System F terms whose contextual equivalence is not preserved by the Sumii-Pierce compiler, nor the embedding into the polymorphic blame calculus. This counterexample relies on the absence in System F of what we call a universal type, i.e., a type that all other types can be injected into and extracted from. As the languages in which System F is compiled have a universal type, the compilation cannot be fully abstract; this paper explains why.

We believe this paper thus sheds light on recent results in the field of gradually typed languages and it provides a perspective for further research into secure compilation of polymorphic languages.

Supplementary Material

Auxiliary Archive (popl18-p46-aux.zip)

This file contains a single PDF file containing the technical appendix described in the article, containing proofs and technical details supporting the results described in the paper.

Download
299.51 KB

WEBM File (parametricityversustheuniversaltype.webm)

Download
137.17 MB

References

[1]

Martín Abadi. 1998. Protection in Programming-Language Translations. In ICALP’98. 868–883.

[2]

Martín Abadi, Luca Cardelli, Benjamin Pierce, and Gordon Plotkin. 1991. Dynamic Typing in a Statically Typed Language. ACM Trans. Program. Lang. Syst. 13, 2 (April 1991), 237–268.

Digital Library

[3]

Martín Abadi, Cédric Fournet, and Georges Gonthier. 1998. Secure Implementation of Channel Abstractions. In IEEE Symposium on Logic in Computer Science. 105–116.

[4]

Martín Abadi, Cédric Fournet, and Georges Gonthier. 1999. Secure Communications Processing for Distributed Languages. In IEEE Symposium on Security and Privacy. 74–88.

[5]

Martín Abadi, Cédric Fournet, and Georges Gonthier. 2000. Authentication Primitives and their Compilation. In Principles of Programming Languages. ACM, 302–315.

Digital Library

[6]

Martín Abadi and Gordon D. Plotkin. 2012. On Protection by Layout Randomization. ACM Transactions on Information and System Security 15, Article 8 (July 2012), 8:1–8:29 pages.

Digital Library

[7]

Pieter Agten, Raoul Strackx, Bart Jacobs, and Frank Piessens. 2012. Secure Compilation to Modern Processors. In Computer Security Foundations Symposium. IEEE, 171–185.

Digital Library

[8]

Amal Ahmed and Matthias Blume. 2008. Typed Closure Conversion Preserves Observational Equivalence. In International Conference on Functional Programming. ACM, 157–168.

Digital Library

[9]

Amal Ahmed, Justin Damner, Jeremy G. Siek, and Philip Wadler. 2017. Theorems for Free for Free. In ICFP.

[10]

Amal Ahmed, Derek Dreyer, and Andreas Rossberg. 2009. State-dependent Representation Independence. In Principles of Programming Languages. ACM, 340–353.

Digital Library

[11]

Amal Ahmed, Robert Bruce Findler, Jeremy G. Siek, and Philip Wadler. 2011a. Blame for All. In Principles of Programming Languages. 201–214.

Digital Library

[12]

Amal Ahmed, Robert Bruce Findler, Jeremy G. Siek, and Philip Wadler. 2011b. Blame for All. Technical Report. https: //plt.eecs.northwestern.edu/blame- for- all/

[13]

Amal Ahmed, Lindsey Kuper, and Jacob Matthews. 2011c. Parametric polymorphism through run-time sealing, or, Theorems for low, low prices! (April 2011). http://www.ccs.neu.edu/home/amal/papers/paramseal- tr.pdf

[14]

Amal Ahmed, Jacob Matthews, Robert Bruce Findler, and Philip Wadler. 2009. Blame for All. In Workshop on Script-to-Program Evolution (STOP). 1–13.

Digital Library

[15]

Robert Atkey, Neil Ghani, and Patricia Johann. 2014. A relationally parametric model of dependent type theory. In Principles of Programming Languages. ACM, 503–515.

Digital Library

[16]

Michele Bugliesi and Marco Giunti. 2007. Secure Implementations of Typed Channel Abstractions. In Principles of Programming Languages. ACM, 251–262.

Digital Library

[17]

Matteo Cimini and Jeremy G. Siek. 2016. The Gradualizer: A Methodology and Algorithm for Generating Gradual Type Systems. In Principles of Programming Languages. ACM.

Digital Library

[18]

Dominique Devriese, Marco Patrignani, and Frank Piessens. 2016. Fully-abstract Compilation by Approximate Backtranslation. In Principles of Programming Languages. 164–177.

[19]

Dominique Devriese, Marco Patrignani, Frank Piessens, and Steven Keuchel. 2017. Modular, Fully-Abstract Compilation by Approximate Back-Translation. to appear in LMCS. (2017). http://arxiv.org/abs/1703.09988

[20]

D. Dreyer, A. Ahmed, and L. Birkedal. 2009. Logical Step-Indexed Logical Relations. In Logic In Computer Science. 71–80.

Digital Library

[21]

Robert Bruce Findler and Matthias Felleisen. 2002. Contracts for Higher-order Functions. In International Conference on Functional Programming. ACM.

Digital Library

[22]

Cedric Fournet, Nikhil Swamy, Juan Chen, Pierre-Evariste Dagand, Pierre-Yves Strub, and Benjamin Livshits. 2013. Fully Abstract Compilation to JavaScript. In Principles of Programming Languages. ACM, 371–384.

Digital Library

[23]

Ronald Garcia, Alison M. Clark, and ÃĽric Tanter. 2016. Abstracting Gradual Typing. In Principles of Programming Languages. ACM.

Digital Library

[24]

Jean-Yves Girard. 1972. Interprétation Fonctionelle et Élimination Des Coupures de l’arithmétique d’ordre Supérieur. Ph.D. Dissertation. Université Paris VII.

[25]

Arjun Guha, Jacob Matthews, Robert Bruce Findler, and Shriram Krishnamurthi. 2007. Relationally-parametric Polymorphic Contracts. In Symposium on Dynamic Languages. ACM.

Digital Library

[26]

Yuu Igarashi, Taro Sekiyama, and Atsushi Igarashi. 2017. On Polymorphic Gradual Typing. In International Conference on Functional Programming. ACM.

Digital Library

[27]

Radha Jagadeesan, Corin Pitcher, Julian Rathke, and James Riely. 2011. Local Memory via Layout Randomization. In Computer Security Foundations Symposium. IEEE Computer Society, 161–174.

Digital Library

[28]

Yannis Juglaret, Cătălin Hriţcu, Arthur Azevedo de Amorim, and Benjamin C. Pierce. 2016. Beyond Good and Evil: Formalizing the Security Guarantees of Compartmentalizing Compilation. In Computer Security Foundations Symposium.

[29]

Yannis Juglaret, Catalin Hritcu, Arthur Azevedo de Amorim, Benjamin C. Pierce, Antal Spector-Zabusky, and Andrew Tolmach. 2015. Towards a Fully Abstract Compiler Using Micro-Policies: Secure Compilation for Mutually Distrustful Components. CoRR abs/1510.00697 (2015). http://arxiv.org/abs/1510.00697

[30]

Adriaan Larmuseau, Marco Patrignani, and Dave Clarke. 2015. A Secure Compiler for ML Modules. In Programming Languages and Systems - 13th Asian Symposium. 29–48.

[31]

Adriaan Larmuseau, Marco Patrignani, and Dave Clarke. 2016. Implementing a Secure Abstract Machine. In Symposium on Applied Computing. ACM, 2041–2048.

Digital Library

[32]

John R. Longley. 2003. Universal Types and What They are Good For. In Domain Theory, Logic and Computation. Springer, Dordrecht, 25–63.

[33]

Jacob Matthews and Amal Ahmed. 2008. Parametric Polymorphism through Run-Time Sealing or, Theorems for Low, Low Prices! LNCS, Vol. 4960. 16–31.

[34]

Jacob Matthews and Robert Bruce Findler. 2009. Operational Semantics for Multi-language Programs. ACM Trans. Program. Lang. Syst. 31, 3 (April 2009), 12:1–12:44.

Digital Library

[35]

James H. Morris, Jr. 1973a. Protection in Programming Languages. Commun. ACM 16, 1 (Jan. 1973), 15–21.

Digital Library

[36]

James H. Morris, Jr. 1973b. Types Are Not Sets. In Principles of Programming Languages. 120–124.

Digital Library

[37]

Georg Neis, Derek Dreyer, and Andreas Rossberg. 2009. Non-parametric Parametricity. In ICFP ’09. 135–148.

Digital Library

[38]

Georg Neis, Derek Dreyer, and Andreas Rossberg. 2011. Non-parametric parametricity. Journal of Functional Programming 21 (2011), 497–562.

Digital Library

[39]

Marco Patrignani, Pieter Agten, Raoul Strackx, Bart Jacobs, Dave Clarke, and Frank Piessens. 2015. Secure Compilation to Protected Module Architectures. ACM Trans. Program. Lang. Syst. 37, Article 6 (April 2015), 6:1–6:50 pages.

Digital Library

[40]

Marco Patrignani, Dominique Devriese, and Frank Piessens. 2016. On Modular and Fully Abstract Compilation. In Computer Security Foundations Symposium.

[41]

Benjamin Pierce. 2002. Types and Programming Languages. MIT Press.

Digital Library

[42]

Benjamin Pierce and Eijiro Sumii. 2000. Relating Cryptography and Polymorphism. (2000). http://www.kb.ecei.tohoku.ac. jp/~sumii/pub/infohide.pdf manuscript.

[43]

Gordon D. Plotkin. 1977. LCF Considered as a Programming Language. Theoretical Computer Science 5 (1977), 223–255.

[44]

John C. Reynolds. 1974. Towards a Theory of Type Structure. In Programming Symposium. Lecture Notes in Computer Science, Vol. 19. Springer-Verlag, 408–423.

[45]

J. C. Reynolds. 1983. Types, Abstraction, and Parametric Polymorphism. In Information Processing. North Holland, 513–523.

[46]

Jeremy Siek and Philip Wadler. 2016. The key to blame: Gradual typing meets cryptography. (2016). http://homepages.inf. ed.ac.uk/wadler/papers/blame- key/blame- key.pdf draft.

[47]

Jeremy G. Siek and Walid Taha. 2006. Gradual Typing for Functional Languages. In SCHEME. 81–92.

[48]

Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, and John Tang Boyland. 2015. Refined Criteria for Gradual Typing. In Summit on Advances in Programming Languages (Leibniz International Proceedings in Informatics (LIPIcs)), Vol. 32. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 274–293.

[49]

Richard Statman. 1991. A local translation of untyped [lambda] calculus into simply typed [lambda] calculus. Technical Report. http://repository.cmu.edu/cgi/viewcontent.cgi?article=1454&context=math

[50]

Christopher Strachey. 2000. Fundamental Concepts in Programming Languages. Higher-Order and Symbolic Computation 13, 1-2 (April 2000), 11–49.

Digital Library

[51]

Eijiro Sumii and Benjamin C. Pierce. 2003. Logical Relations for Encryption. J. Comput. Secur. 11, 4 (July 2003), 521–554.

[52]

Eijiro Sumii and Benjamin C. Pierce. 2004. A Bisimulation for Dynamic Sealing. In Principles of Programming Languages. 161–172.

Digital Library

[53]

Asumu Takikawa, Daniel Feltey, Ben Greenman, Max S. New, Jan Vitek, and Matthias Felleisen. 2016. Is Sound Gradual Typing Dead?. In Principles of Programming Languages. ACM.

Digital Library

[54]

Philip Wadler. 1989. Theorems for Free!. In Functional Programming Languages and Computer Architecture. ACM, 347–359.

Digital Library

[55]

Philip Wadler. 2007. The Girard-Reynolds isomorphism (second edition). Theoretical Computer Science 375, 1 (2007).

Digital Library

[56]

Philip Wadler and Robert Bruce Findler. 2009. Well-Typed Programs Can’t Be Blamed. In Programming Languages and Systems. Springer, Berlin, Heidelberg, 1–16.

Digital Library

[57]

R. N. M. Watson, J. Woodruff, P. G. Neumann, S. W. Moore, J. Anderson, D. Chisnall, N. Dave, B. Davis, K. Gudka, B. Laurie, S. J. Murdoch, R. Norton, M. Roe, S. Son, and M. Vadera. 2015. CHERI: A Hybrid Capability-System Architecture for Scalable Software Compartmentalization. In IEEE Symposium on Security and Privacy.

Digital Library

Cited By

Greenman B(2023)GTP Benchmarks for Gradual Typing PerformanceProceedings of the 2023 ACM Conference on Reproducibility and Replicability10.1145/3589806.3600034(102-114)Online publication date: 27-Jun-2023
https://dl.acm.org/doi/10.1145/3589806.3600034
Labrada EToro MTanter É(2022)Gradual System FJournal of the ACM10.1145/355598669:5(1-78)Online publication date: 28-Oct-2022
https://dl.acm.org/doi/10.1145/3555986
Devriese DPatrignani MPiessens F(2022)Two Parametricities Versus Three Universal TypesACM Transactions on Programming Languages and Systems10.1145/353965744:4(1-43)Online publication date: 21-Sep-2022
https://dl.acm.org/doi/10.1145/3539657
Show More Cited By

Index Terms

Parametricity versus the universal type
1. Security and privacy
  1. Formal methods and theory of security
    1. Formal security models
    2. Logic and verification
2. Theory of computation
  1. Logic
    1. Logic and verification

Recommendations

Graduality and parametricity: together again for the first time

Parametric polymorphism and gradual typing have proven to be a difficult combination, with no language yet produced that satisfies the fundamental theorems of each: parametricity and graduality. Notably, Toro, Labrada, and Tanter (POPL 2019) conjecture ...
Gradual parametricity, revisited

Bringing the benefits of gradual typing to a language with parametric polymorphism like System F, while preserving relational parametricity, has proven extremely challenging: first attempts were formulated a decade ago, and several designs were recently ...
Theorems for free for free: parametricity, with and without types

The polymorphic blame calculus integrates static typing, including universal types, with dynamic typing. The primary challenge with this integration is preserving parametricity: even dynamically-typed code should satisfy it once it has been cast to a ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 2, Issue POPL

January 2018

1961 pages

EISSN:2475-1421

DOI:10.1145/3177123

Issue’s Table of Contents

Copyright © 2017 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]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 27 December 2017

Published in PACMPL Volume 2, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

13
Total Citations
View Citations
681
Total Downloads

Downloads (Last 12 months)108
Downloads (Last 6 weeks)13

Reflects downloads up to 09 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Greenman B(2023)GTP Benchmarks for Gradual Typing PerformanceProceedings of the 2023 ACM Conference on Reproducibility and Replicability10.1145/3589806.3600034(102-114)Online publication date: 27-Jun-2023
https://dl.acm.org/doi/10.1145/3589806.3600034
Labrada EToro MTanter É(2022)Gradual System FJournal of the ACM10.1145/355598669:5(1-78)Online publication date: 28-Oct-2022
https://dl.acm.org/doi/10.1145/3555986
Devriese DPatrignani MPiessens F(2022)Two Parametricities Versus Three Universal TypesACM Transactions on Programming Languages and Systems10.1145/353965744:4(1-43)Online publication date: 21-Sep-2022
https://dl.acm.org/doi/10.1145/3539657
Labrada EToro MTanter ÉDevriese D(2022)Plausible sealing for gradual parametricityProceedings of the ACM on Programming Languages10.1145/35273146:OOPSLA1(1-28)Online publication date: 29-Apr-2022
https://dl.acm.org/doi/10.1145/3527314
Patrignani MGarg D(2021)Robustly Safe Compilation, an Efficient Form of Secure CompilationACM Transactions on Programming Languages and Systems10.1145/343680943:1(1-41)Online publication date: 9-Feb-2021
https://dl.acm.org/doi/10.1145/3436809
Jacobs KTimany ADevriese D(2021)Fully abstract from static to gradualProceedings of the ACM on Programming Languages10.1145/34342885:POPL(1-30)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434288
Ngo MNaumann DRezk T(2020)Type-Based Declassification for FreeFormal Methods and Software Engineering10.1007/978-3-030-63406-3_11(181-197)Online publication date: 19-Dec-2020
https://doi.org/10.1007/978-3-030-63406-3_11
Xie NBi XOliveira BSchrijvers T(2019)Consistent Subtyping for AllACM Transactions on Programming Languages and Systems10.1145/331033942:1(1-79)Online publication date: 21-Nov-2019
https://dl.acm.org/doi/10.1145/3310339
Toro MLabrada ETanter É(2019)Gradual parametricity, revisitedProceedings of the ACM on Programming Languages10.1145/32903303:POPL(1-30)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290330
Omar CVoysey IChugh RHammer M(2019)Live functional programming with typed holesProceedings of the ACM on Programming Languages10.1145/32903273:POPL(1-32)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290327
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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 Article

Media

Figures

Other

Tables

View Issue’s Table of Contents