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

research-article

Gradual refinement types

Authors:

Éric TanterAuthors Info & Claims

ACM SIGPLAN Notices, Volume 52, Issue 1

Pages 775 - 788

https://doi.org/10.1145/3093333.3009856

Published: 01 January 2017 Publication History

Abstract

Refinement types are an effective language-based verification technique. However, as any expressive typing discipline, its strength is its weakness, imposing sometimes undesired rigidity. Guided by abstract interpretation, we extend the gradual typing agenda and develop the notion of gradual refinement types, allowing smooth evolution and interoperability between simple types and logically-refined types. In doing so, we address two challenges unexplored in the gradual typing literature: dealing with imprecise logical information, and with dependent function types. The first challenge leads to a crucial notion of locality for refinement formulas, and the second yields novel operators related to type- and term-level substitution, identifying new opportunity for runtime errors in gradual dependently-typed languages. The gradual language we present is type safe, type sound, and satisfies the refined criteria for gradually-typed languages of Siek et al. We also explain how to extend our approach to richer refinement logics, anticipating key challenges to consider.

References

[1]

F. Bañados Schwerter, R. Garcia, and É. Tanter. A theory of gradual effect systems. In 19th ACM SIGPLAN Conference on Functional Programming (ICFP 2014), pages 283–295, Gothenburg, Sweden, Sept. 2014. ACM Press.

Digital Library

[2]

F. Bañados Schwerter, R. Garcia, and É. Tanter. Gradual type-and-effect systems. Journal of Functional Programming, 26:19:1–19:69, Sept. 2016.

[3]

J. Bengtson, K. Bhargavan, C. Fournet, A. D. Gordon, and S. Maffeis. Refinement types for secure implementations. ACM Transactions on Programming Languages and Systems, 33(2):8:1–8:45, Jan. 2011.

Digital Library

[4]

R. Chugh. Nested Refinement Types for JavaScript. PhD thesis, University of California, Sept. 2013.

[5]

R. Chugh, D. Herman, and R. Jhala. Dependent types for JavaScript. In 27th ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 2012), pages 587–606, Tucson, AZ, USA, Oct. 2012a. ACM Press.

Digital Library

[6]

R. Chugh, P. M. Rondon, A. Bakst, and R. Jhala. Nested refinements: a logic for duck typing. In 39th annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2012), pages 231–244, Philadelphia, USA, Jan. 2012b. ACM Press.

Digital Library

[7]

A. Church. A formulation of the simple theory of types. J. Symbolic Logic, 5(2):56–68, 06 1940.

[8]

P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In 4th ACM Symposium on Principles of Programming Languages (POPL 77), pages 238–252, Los Angeles, CA, USA, Jan. 1977.

Digital Library

[9]

ACM Press.

[10]

T. Disney and C. Flanagan. Gradual information flow typing. In International Workshop on Scripts to Programs, 2011.

[11]

L. Fennell and P. Thiemann. Gradual security typing with references. In Computer Security Foundations Symposium, pages 224–239, June 2013.

Digital Library

[12]

R. B. Findler and M. Felleisen. Contracts for higher-order functions. In 7th ACM SIGPLAN Conference on Functional Programming (ICFP 2002), pages 48–59, Pittsburgh, PA, USA, Sept. 2002. ACM Press.

Digital Library

[13]

C. Flanagan. Hybrid type checking. In 33th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2006), pages 245–256, Charleston, SC, USA, Jan. 2006. ACM Press.

Digital Library

[14]

T. Freeman and F. Pfenning. Refinement types for ML. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’91), pages 268–277. ACM Press, 1991.

Digital Library

[15]

R. Garcia and M. Cimini. Principal type schemes for gradual programs. In 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2015), pages 303–315. ACM Press, Jan. 2015.

Digital Library

[16]

R. Garcia, A. M. Clark, and É. Tanter. Abstracting gradual typing. In 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016), St Petersburg, FL, USA, Jan. 2016. ACM Press.

Digital Library

[17]

M. Greenberg, B. C. Pierce, and S. Weirich. Contracts made manifest. In 37th annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2010), pages 353–364. ACM Press, Jan. 2010.

Digital Library

[18]

J. Gronski and C. Flanagan. Unifying hybrid types and contracts. In Trends in Functional Programming, pages 54–70, 2007.

[19]

W. A. Howard. The formulae-as-types notion of construction. In J. P. Seldin and J. R. Hindley, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, pages 479–490. Academic Press, New York, 1980. Reprint of 1969 article. M. Kawaguchi, P. Rondon, and R. Jhala. Type-based data structure verification. In Proceedings of the 30th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2009), pages 304–315. ACM Press, June 2009.

Digital Library

[20]

K. Knowles and C. Flanagan. Hybrid type checking. ACM Trans. Program. Lang. Syst., 32(2), 2010.

Digital Library

[21]

N. Lehmann and É. Tanter. Gradual refinement types – extended version with proofs. Technical Report TR/DCC-2016-1, University of Chile, Nov. 2016.

[22]

A. Miné. Weakly Relational Numerical Abstract Domains. PhD thesis, L’École Polythechnique, Dec. 2004.

[23]

X. Ou, G. Tan, Y. Mandelbaum, and D. Walker. Dynamic typing with dependent types. In Proceedings of the IFIP International Conference on Theoretical Computer Science, pages 437–450, 2004.

[24]

P. M. Rondon, M. Kawaguci, and R. Jhala. Liquid types. In 29th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2008), pages 159–169, Tucson, AZ, USA, June 2008.

Digital Library

[25]

ACM Press.

[26]

J. G. Siek and W. Taha. Gradual typing for functional languages. In Scheme and Functional Programming Workshop, pages 81–92, Sept. 2006.

[27]

J. G. Siek, M. M. Vitousek, M. Cimini, and J. T. Boyland. Refined criteria for gradual typing. In 1st Summit on Advances in Programming Languages (SNAPL 2015), pages 274–293, 2015.

[28]

M. Sozeau. Subset coercions in Coq. In Types for Proofs and Programs, volume 4502 of LNCS, pages 237–252. Springer-Verlag, 2007.

Digital Library

[29]

N. Swamy, C. Hritcu, C. Keller, A. Rastogi, A. Delignat-Lavaud, S. Forest, K. Bhargavan, C. Fournet, P.-Y. Strub, M. Kohlweiss, J. K. Zinzindohoue, and S. Zanella Béguelin. Dependent types and multi-effects in F. In 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016), pages 256–270, St Petersburg, FL, USA, Jan. 2016. ACM Press.

Digital Library

[30]

É. Tanter and N. Tabareau. Gradual certified programming in Coq. In Proceedings of the 11th ACM Dynamic Languages Symposium (DLS 2015), pages 26–40, Pittsburgh, PA, USA, Oct. 2015. ACM Press.

Digital Library

[31]

P. Thiemann and L. Fennell. Gradual typing for annotated type systems. In Z. Shao, editor, 23rd European Symposium on Programming Languages and Systems (ESOP 2014), volume 8410 of LNCS, pages 47–66, Grenoble, France, 2014. Springer-Verlag.

Digital Library

[32]

N. Vazou, P. M. Rondon, and R. Jhala. Abstract refinement types. In M. Felleisen and P. Gardner, editors, Proceedings of the 22nd European Symposium on Programming Languages and Systems (ESOP 2013), volume 7792 of LNCS, pages 209–228, Rome, Italy, Mar. 2013. Springer-Verlag.

Digital Library

[33]

N. Vazou, E. L. Seidel, R. Jhala, D. Vytiniotis, and S. L. P. Jones. Refinement types for haskell. In 19th ACM SIGPLAN Conference on Functional Programming (ICFP 2014), pages 269–282, Gothenburg, Sweden, Sept. 2014. ACM Press.

Digital Library

[34]

N. Vazou, A. Bakst, and R. Jhala. Bounded refinement types. In 20th ACM SIGPLAN Conference on Functional Programming (ICFP 2015), pages 48–61, Vancouver, Canada, Sept. 2015. ACM Press.

Digital Library

[35]

P. Vekris, B. Cosman, and R. Jhala. Refinement types for TypeScript. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2016), pages 310–325, Santa Barbara, CA, USA, June 2016. ACM Press.

Digital Library

[36]

H. Xi and F. Pfenning. Eliminating array bound checking through dependent types. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’98), pages 249–257. ACM Press, 1998.

Digital Library

Cited By

Lemay MFu QBlair WZhang CXi HCong YDagand P(2023)A Dependently Typed Language with Dynamic EqualityProceedings of the 8th ACM SIGPLAN International Workshop on Type-Driven Development10.1145/3609027.3609407(44-57)Online publication date: 30-Aug-2023
https://dl.acm.org/doi/10.1145/3609027.3609407
Ye WToro MOlmedo F(2023)A Gradual Probabilistic Lambda CalculusProceedings of the ACM on Programming Languages10.1145/35860367:OOPSLA1(256-285)Online publication date: 6-Apr-2023
https://doi.org/10.1145/3586036
Kura S(2021)A General Semantic Construction of Dependent Refinement Type Systems, CategoricallyFoundations of Software Science and Computation Structures10.1007/978-3-030-71995-1_21(406-426)Online publication date: 23-Mar-2021
https://doi.org/10.1007/978-3-030-71995-1_21
Show More Cited By

Index Terms

Gradual refinement types
1. Software and its engineering
  1. Software notations and tools
    1. Formal language definitions
2. Theory of computation
  1. Formal languages and automata theory

Recommendations

Gradual refinement types
POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages

Refinement types are an effective language-based verification technique. However, as any expressive typing discipline, its strength is its weakness, imposing sometimes undesired rigidity. Guided by abstract interpretation, we extend the gradual typing ...
Sums of uncertainty: refinements go gradual
POPL '17

A long-standing shortcoming of statically typed functional languages is that type checking does not rule out pattern-matching failures (run-time match exceptions). Refinement types distinguish different values of datatypes; if a program annotated with ...
Gradual typing with union and intersection types

We propose a type system for functional languages with gradual types and set-theoretic type connectives and prove its soundness. In particular, we show how to lift the definition of the domain and result type of an application from non-gradual types to ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 52, Issue 1

POPL '17

January 2017

901 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/3093333

Editor:
Matthew Fluet

Issue’s Table of Contents

POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages
January 2017
901 pages
ISBN:9781450346603
DOI:10.1145/3009837
General Chair:
Giuseppe Castagna
Paris Diderot University, France / CNRS, France
,
Program Chair:
Andrew D. Gordon
Microsoft Research, UK / University of Edinburgh, UK

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 the author(s) 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: 01 January 2017

Published in SIGPLAN Volume 52, Issue 1

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

29
Total Citations
View Citations
546
Total Downloads

Downloads (Last 12 months)42
Downloads (Last 6 weeks)4

Reflects downloads up to 12 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Lemay MFu QBlair WZhang CXi HCong YDagand P(2023)A Dependently Typed Language with Dynamic EqualityProceedings of the 8th ACM SIGPLAN International Workshop on Type-Driven Development10.1145/3609027.3609407(44-57)Online publication date: 30-Aug-2023
https://dl.acm.org/doi/10.1145/3609027.3609407
Ye WToro MOlmedo F(2023)A Gradual Probabilistic Lambda CalculusProceedings of the ACM on Programming Languages10.1145/35860367:OOPSLA1(256-285)Online publication date: 6-Apr-2023
https://doi.org/10.1145/3586036
Kura S(2021)A General Semantic Construction of Dependent Refinement Type Systems, CategoricallyFoundations of Software Science and Computation Structures10.1007/978-3-030-71995-1_21(406-426)Online publication date: 23-Mar-2021
https://doi.org/10.1007/978-3-030-71995-1_21
New MGiovannini ELicata D(2023)Gradual Typing for Effect HandlersProceedings of the ACM on Programming Languages10.1145/36228607:OOPSLA2(1758-1786)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622860
Hattori MKobayashi NSato R(2023)Gradual Tensor Shape CheckingProgramming Languages and Systems10.1007/978-3-031-30044-8_8(197-224)Online publication date: 22-Apr-2023
https://dl.acm.org/doi/10.1007/978-3-031-30044-8_8
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
Maillard KLennon-Bertrand MTabareau NTanter É(2022)A reasonably gradual type theoryProceedings of the ACM on Programming Languages10.1145/35476556:ICFP(931-959)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3547655
Eremondi JGarcia RTanter É(2022)Propositional equality for gradual dependently typed programmingProceedings of the ACM on Programming Languages10.1145/35476276:ICFP(165-193)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3547627
Chen ZAmin NIII H(2022)A Hoare logic style refinement types formalisationProceedings of the 7th ACM SIGPLAN International Workshop on Type-Driven Development10.1145/3546196.3550162(1-14)Online publication date: 6-Sep-2022
https://dl.acm.org/doi/10.1145/3546196.3550162
Lennon-Bertrand MMaillard KTabareau NTanter É(2022)Gradualizing the Calculus of Inductive ConstructionsACM Transactions on Programming Languages and Systems10.1145/349552844:2(1-82)Online publication date: 6-Apr-2022
https://dl.acm.org/doi/10.1145/3495528
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 Issue’s Table of Contents