research-article

Nested refinements: a logic for duck typing

Authors:

Patrick M. Rondon,

Ranjit JhalaAuthors Info & Claims

ACM SIGPLAN Notices, Volume 47, Issue 1

Pages 231 - 244

https://doi.org/10.1145/2103621.2103686

Published: 25 January 2012 Publication History

Abstract

Programs written in dynamic languages make heavy use of features --- run-time type tests, value-indexed dictionaries, polymorphism, and higher-order functions --- that are beyond the reach of type systems that employ either purely syntactic or purely semantic reasoning. We present a core calculus, System D, that merges these two modes of reasoning into a single powerful mechanism of nested refinement types wherein the typing relation is itself a predicate in the refinement logic. System D coordinates SMT-based logical implication and syntactic subtyping to automatically typecheck sophisticated dynamic language programs. By coupling nested refinements with McCarthy's theory of finite maps, System D can precisely reason about the interaction of higher-order functions, polymorphism, and dictionaries. The addition of type predicates to the refinement logic creates a circularity that leads to unique technical challenges in the metatheory, which we solve with a novel stratification approach that we use to prove the soundness of System D.

Supplementary Material

JPG File (popl_4a_2.jpg)

Download
11.31 KB

MP4 File (popl_4a_2.mp4)

Download
290.36 MB

References

[1]

M. Abadi, L. Cardelli, B. C. Pierce, and G. Plotkin. Dynamic typing in a statically-typed language. In POPL, 1989.

Digital Library

[2]

J.-h. D. An, A. Chaudhuri, J. S. Foster, and M. Hicks. Dynamic inference of static types for ruby. In POPL, 2011.

Digital Library

[3]

C. Anderson, S. Drossopoulou, and P. Giannini. Towards Type Inference for JavaScript. In ECOOP, pages 428--452, June 2005.

Digital Library

[4]

J. Bengtson, K. Bhargavan, C. Fournet, A. Gordon, and S. Maffeis. Refinement types for secure implementations. In CSF, 2008.

Digital Library

[5]

Y. Bertot and P. Castéran. Interactive theorem proving and program development. coq'art: The calculus of inductive constructions, 2004.

Digital Library

[6]

G. M. Bierman, A. D. Gordon, C. Hritcu, and D. E. Langworthy. Semantic subtyping with an smt solver. In ICFP, 2010.

Digital Library

[7]

A. R. Bradley, Z. Manna, and H. B. Sipma. What's decidable about arrays? In VMCAI, pages 427--442, 2006.

Digital Library

[8]

R. Chugh, P. M. Rondon, and R. Jhala. Nested refinements: A logic for duck typing. http://arxiv.org/abs/1103.5055v2.

[9]

R. Chugh, J. A. Meister, R. Jhala, and S. Lerner. Staged information flow for javascript. In Proceedings of PLDI 2009, pages 50--62, 2009.

Digital Library

[10]

J. Condit, B. Hackett, S. K. Lahiri, and S. Qadeer. Unifying type checking and property checking for low-level code. In POPL, 2009.

Digital Library

[11]

R. Davies. Practical Refinement-Type Checking. PhD thesis, Carnegie Mellon University, Pittsburgh, PA, USA, 2005.

Digital Library

[12]

L. de Moura and N. Bjørner. Z3: An efficient SMT solver. In TACAS, 2008.

Digital Library

[13]

L. de Moura and N. Bjørner. Generalized, efficient array decision procedures. In FMCAD, pages 45--52, 2009.

[14]

J. Dunfield. A Unified System of Type Refinements. PhD thesis, Carnegie Mellon University, Pittsburgh, PA, USA, 2007.

[15]

R. B. Findler and M. Felleisen. Contracts for higher-order functions. In ICFP, pages 48--59, 2002.

Digital Library

[16]

C. Flanagan. Hybrid type checking. In POPL. ACM, 2006.

Digital Library

[17]

M. Furr, J. hoon (David) An, J. S. Foster, and M. W. Hicks. Static type inference for ruby. In SAC, pages 1859--1866, 2009.

Digital Library

[18]

A. Guha, C. Softoiu, and S. Krishnamurthi. Typing local control and state using flow analysis. In ESOP, 2011.

Digital Library

[19]

P. Heidegger and P. Thiemann. Recency types for analyzing scripting languages. In ECOOP, pages 200--224, 2010.

Digital Library

[20]

P. Hooimeijer and M. Veanes. An evaluation of automata algorithms for string analysis. In VMCAI, pages 248--262, 2011.

Digital Library

[21]

R. Jhala, R. Majumdar, and R.-G. Xu. State of the union: Type inference via craig interpolation. In TACAS, 2007.

Digital Library

[22]

A. J. Kennedy and B. C. Pierce. On decidability of nominal subtyping with variance. In FOOL-WOOD, 2007.

[23]

K. Knowles and C. Flanagan. Hybrid type checking. ACM TOPLAS, 32 (2), 2010.

Digital Library

[24]

R. Komondoor, G. Ramalingam, S. Chandra, and J. Field. Dependent types for program understanding. In TACAS, pages 157--173, 2005.

Digital Library

[25]

J. McCarthy. Towards a mathematical science of computation. In In IFIP Congress, pages 21--28. North-Holland, 1962.

[26]

G. Nelson and D. C. Oppen. Simplification by cooperating decision procedures. TOPLAS, 1979.

Digital Library

[27]

X. Ou, G. Tan, Y. Mandelbaum, and D. Walker. Dynamic typing with dependent types. In IFIP TCS, pages 437--450, 2004.

[28]

J. Palsberg and M. I. Schwartzbach. OO Type Systems. Wiley, 1994.

[29]

B. C. Pierce and D. N. Turner. Local type inference. In POPL, pages 252--265, 1998.

Digital Library

[30]

D. Rémy. Type checking records and variants in a natural extension of ml. In POPL, 1989.

Digital Library

[31]

P. Rondon, M. Kawaguchi, and R. Jhala. Liquid types. In PLDI, 2008.

Digital Library

[32]

P. Rondon, M. Kawaguchi, and R. Jhala. Low-level liquid types. In POPL, pages 131--144, 2010.

Digital Library

[33]

R. Shostak. Deciding combinations of theories. Journal of the ACM, 31 (1): 1--12, 1984.

Digital Library

[34]

J. Siek and W. Taha. Gradual typing for functional languages. In Scheme and Functional Programming Workshop, 2006.

[35]

N. Swamy, J. Chen, and R. Chugh. Enforcing stateful authorization and information flow policies in fine. In ESOP, 2010.

Digital Library

[36]

The Dojo Foundation. Dojo toolkit. http://dojotoolkit.org/.

[37]

}python-32The Python Software Foundation. Python 3.2 standard library. http://python.org/.

[38]

P. Thiemann. Towards a type system for analyzing javascript programs. In ESOP, 2005.

Digital Library

[39]

S. Tobin-Hochstadt and M. Felleisen. Logical types for untyped languages. In ICFP, pages 117--128, 2010.

Digital Library

[40]

H. Xi and F. Pfenning. Dependent types in practical programming. In POPL, 1999.

Digital Library

[41]

T. Zhao. Type inference for scripting languages with implicit extension. In FOOL, 2010.

Cited By

Hu MZhang Y(2022)An empirical study of the Python/C API on evolution and bug patternsJournal of Software: Evolution and Process10.1002/smr.2507Online publication date: 6-Sep-2022
https://doi.org/10.1002/smr.2507
Cuadrado JGuerra Ede Lara J(2017)Static Analysis of Model TransformationsIEEE Transactions on Software Engineering10.1109/TSE.2016.263513743:9(868-897)Online publication date: 14-Sep-2017
https://dl.acm.org/doi/10.1109/TSE.2016.2635137
Dal Sasso TMocci ALanza M(2015)Misery loves company: CrowdStacking traces to aid problem detection2015 IEEE 22nd International Conference on Software Analysis, Evolution, and Reengineering (SANER)10.1109/SANER.2015.7081823(131-140)Online publication date: Mar-2015
https://doi.org/10.1109/SANER.2015.7081823
Show More Cited By

Index Terms

Nested refinements: a logic for duck typing
1. Theory of computation
  1. Logic
    1. Programming logic
  2. Semantics and reasoning
    1. Program reasoning

Recommendations

Nested refinements: a logic for duck typing
POPL '12: Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Programs written in dynamic languages make heavy use of features --- run-time type tests, value-indexed dictionaries, polymorphism, and higher-order functions --- that are beyond the reach of type systems that employ either purely syntactic or purely ...
Temporal Refinements for Guarded Recursive Types
Programming Languages and Systems
Abstract
We propose a logic for temporal properties of higher-order programs that handle infinite objects like streams or infinite trees, represented via coinductive types. Specifications of programs use safety and liveness properties. Programs can then be ...
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 ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 47, Issue 1

POPL '12

January 2012

569 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/2103621

Issue’s Table of Contents

POPL '12: Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
January 2012
602 pages
ISBN:9781450310833
DOI:10.1145/2103656
General Chair:
John Field
Google, USA
,
Program Chair:
Michael Hicks
University of Maryland, College Park, USA

Copyright © 2012 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: 25 January 2012

Published in SIGPLAN Volume 47, Issue 1

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

67
Total Citations
View Citations
612
Total Downloads

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

Reflects downloads up to 08 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Hu MZhang Y(2022)An empirical study of the Python/C API on evolution and bug patternsJournal of Software: Evolution and Process10.1002/smr.2507Online publication date: 6-Sep-2022
https://doi.org/10.1002/smr.2507
Cuadrado JGuerra Ede Lara J(2017)Static Analysis of Model TransformationsIEEE Transactions on Software Engineering10.1109/TSE.2016.263513743:9(868-897)Online publication date: 14-Sep-2017
https://dl.acm.org/doi/10.1109/TSE.2016.2635137
Dal Sasso TMocci ALanza M(2015)Misery loves company: CrowdStacking traces to aid problem detection2015 IEEE 22nd International Conference on Software Analysis, Evolution, and Reengineering (SANER)10.1109/SANER.2015.7081823(131-140)Online publication date: Mar-2015
https://doi.org/10.1109/SANER.2015.7081823
Cox AChang BRival X(2015)Desynchronized Multi-State Abstractions for Open Programs in Dynamic LanguagesProceedings of the 24th European Symposium on Programming on Programming Languages and Systems - Volume 903210.1007/978-3-662-46669-8_20(483-509)Online publication date: 11-Apr-2015
https://dl.acm.org/doi/10.1007/978-3-662-46669-8_20
Cox AChang BRival X(2014)Automatic Analysis of Open Objects in Dynamic Language ProgramsStatic Analysis10.1007/978-3-319-10936-7_9(134-150)Online publication date: 2014
https://doi.org/10.1007/978-3-319-10936-7_9
Bjørner N(2012)Taking satisfiability to the next level with z3Proceedings of the 6th international joint conference on Automated Reasoning10.1007/978-3-642-31365-3_1(1-8)Online publication date: 26-Jun-2012
https://dl.acm.org/doi/10.1007/978-3-642-31365-3_1
CAMPORA JCHEN SERWIG MWALKINGSHAW E(2022)Migrating gradual typesJournal of Functional Programming10.1017/S095679682200008932Online publication date: 6-Oct-2022
https://doi.org/10.1017/S0956796822000089
Castagna GLanvin VLaurent MNguyen K(2022)Revisiting occurrence typingScience of Computer Programming10.1016/j.scico.2022.102781217:COnline publication date: 1-May-2022
https://dl.acm.org/doi/10.1016/j.scico.2022.102781
Hu MZhang Y(2022)An empirical study of the Python/C API on evolution and bug patternsJournal of Software: Evolution and Process10.1002/smr.250735:2Online publication date: 6-Sep-2022
https://doi.org/10.1002/smr.2507
Nguyễn PGilray TTobin-Hochstadt SVan Horn D(2017)Soft contract verification for higher-order stateful programsProceedings of the ACM on Programming Languages10.1145/31581392:POPL(1-30)Online publication date: 27-Dec-2017
https://dl.acm.org/doi/10.1145/3158139
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.

Figures

Tables

Media

View Issue’s Table of Contents