skip to main content
10.1145/1292597.1292602acmconferencesArticle/Chapter ViewAbstractPublication PagespoplConference Proceedingsconference-collections
Article

Refined typechecking with Stardust

Published: 02 October 2007 Publication History

Abstract

We present Stardust, an implementation of a type system for a subset of ML with type refinements, intersection types, and union types, enabling programmers to legibly specify certain classes of program invariants that are verified at compile time. This is the first implementation of unrestricted intersection and union types in a mainstream functional programming setting, as well as the first implementation of a system with both datasort and index refinements. The system-with the assistance of external constraint solvers-supports integer, Boolean and dimensional index refinements; we apply both value refinements (to check red-black tree invariants) and invaluable refinements (to check dimensional consistency). While typechecking with intersection and union types is intrinsically complex, our experience so far suggests that it can be practical in many instances.

References

[1]
Roberto Amadio and Pierre-Louis Curien. Domains and lambda calculi, volume 46 of Cambridge Tracts in Theoretical Comp. Sci., chapter 3. Cambridge Univ. Press, 1998.
[2]
Lennart Augustsson. Cayenne - a language with dependent types. In ICFP, pages 239--250, 1998.
[3]
Adam Bakewell, Sébastien Carlier, A. J. Kfoury, and J. B. Wells. Inferring intersection typings that are equivalent to call-by-name and call-by-value evaluations. Technical report, Church Project, Boston University, 2005.
[4]
Clark Barrett and Sergey Berezin. CVC Lite: A new implementation of the Cooperating Validity Checker. In Int'l Conf. Computer Aided Verification (CAV '04), pages 515--518, 2004.
[5]
Clark W. Barrett, David L. Dill, and Jeremy R. Levitt. Validity checking for combinations of theories with equality. In Int'l Conf. Formal Methods in Computer-Aided Design (FMCAD '96), pages 187--201, 1996.
[6]
Matthias Blume. No-longer-foreign: Teaching an ML compiler to speak C "natively". Elect. Notes in Theoretical Comp. Sci., 59(1), 2001.
[7]
Chiyan Chen and Hongwei Xi. Combining programming with theorem proving. In ICFP, pages 66--77, 2005.
[8]
James Cheney and Ralf Hinze. First-class phantom types. Technical Report CUCIS TR2003-1901, Cornell University, 2003.
[9]
M. Coppo, M. Dezani-Ciancaglini, and B. Venneri. Functional characters of solvable terms. Zeitschrift f. math. Logik und Grundlagen d. Math., 27:45--58, 1981.
[10]
Thomas H. Cormen, Charles E. Leiserson, and Ronald L. Rivest. Introduction to Algorithms. MIT Press, 1990.
[11]
Rowan Davies. Practical refinement-type checking. PhD thesis, Carnegie Mellon University, 2005. CMU-CS-05-110.
[12]
Rowan Davies and Frank Pfenning. Intersection types and computational effects. In ICFP, pages 198--208, 2000.
[13]
Leonardo de Moura, Sam Owre, Harald Rueß, John Rushby, and Natarajan Shankar. The ICS decision procedures for embedded deduction. In Int'l Joint Conf. Automated Reasoning (IJCAR '04), pages 218--222, 2004.
[14]
Jana Dunfield. A Unified System of Type Refinements. PhD thesis, Carnegie Mellon University, 2007. CMU-CS-07-129. To appear; latest version at https://research.cs.queensu.ca/home/jana/papers/thesis/.
[15]
Jana Dunfield and Frank Pfenning. Type assignment for intersections and unions in call-by-value languages. In Found. Software Science and Computation Structures (FOSSACS '03), pages 250--266, 2003.
[16]
Jana Dunfield and Frank Pfenning. Tridirectional typechecking. In POPL, pages 281--292, January 2004.
[17]
Edward A. Euler, Steven D. Jolly, and H. H. 'Lad' Curtis. The failures of the Mars Climate Orbiter and Mars Polar Lander: a perspective from the people involved. In AAS Guidance and Control Conf., 2001. http://brain.cs.uiuc.edu/integration/AAS01_MCO_MPL_final.pdf.
[18]
Sigbjorn Finne, Daan Leijen, Erik Meijer, and Simon Peyton Jones. Calling hell from heaven and heaven from hell. In ICFP, pages 114--125, 1999.
[19]
Matthew Fluet and Riccardo Pucella. Phantom types and subtyping. ArXiv postprint, http://arxiv.org/abs/cs.PL/043034, January 2006.
[20]
Jeffrey Scott Foster. Type qualifiers: lightweight specifications to improve software quality. PhD thesis, University of California, Berkeley, 2002.
[21]
Tim Freeman and Frank Pfenning. Refinement types for ML. In PLDI, pages 268--277. ACM Press, 1991.
[22]
Stefan Kahrs. Red-black trees with types. J. Functional Programming, 11(4):425--432, 2001.
[23]
Andrew Kennedy. Programming languages and dimensions. PhD thesis, University of Cambridge, 1996.
[24]
Daan Leijen and Erik Meijer. Domain specific embedded compilers. In USENIX Conf. Domain-Specific Languages (DSL '99), pages 109--122, 1999.
[25]
K. Rustan M. Leino. Extended Static Checking: A ten-year perspective. In Dagstuhl Anniversary Conf., pages 157--175, 2001.
[26]
Daniel R. Licata and Robert Harper. A formulation of Dependent ML with explicit equality proofs. Technical Report CMU-CS-05-178, Carnegie Mellon University, 2005.
[27]
Yitzhak Mandelbaum, David Walker, and Robert Harper. An effective theory of type refinements. In ICFP, pages 213--226, 2003.
[28]
Conor McBride and James McKinna. The view from the left. J. Functional Programming, 14(1):69--111, 2004.
[29]
Robin Milner. A theory of type polymorphism in programming. J. Computer and System Sciences, 17(3):348--375, 1978.
[30]
Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. The Definition of Standard ML (Revised). MIT Press, 1997.
[31]
Chris Okasaki. Purely Functional Data Structures. Cambridge, 1998.
[32]
Jens Palsberg and Christina Pavlopoulou. From polyvariant flow information to intersection and union types. J. Functional Programming, 11 (3):263--317, 2001.
[33]
Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey Washburn. Simple unification-based type inference for GADTs. In ICFP, 2006.
[34]
Benjamin C. Pierce. Programming with intersection types, union types, and polymorphism. Technical Report CMU-CS-91-106, Carnegie Mellon University, 1991.
[35]
Benjamin C. Pierce and David N. Turner. Local type inference. In POPL, pages 252--265, 1998. Full version in ACM Trans. Prog. Lang. Sys., 22(1):1--44, 2000.
[36]
Dag Prawitz. Natural Deduction. Almqvist & Wiksells, 1965.
[37]
John C. Reynolds. Types, abstraction, and parametric polymorphism. In Information Processing 83, pages 513--523. Elsevier, 1983. http://www.cs.cmu.edu/afs/cs/user/jcr/ftp/typesabpara.pdf.
[38]
John C. Reynolds. Design of the programming language Forsythe. Technical Report CMU-CS-96-146, Carnegie Mellon University, 1996.
[39]
Tim Sheard. Languages of the future. SIGPLAN Notices, 39(12):119--132, 2004. OOPSLA '04.
[40]
Aaron Stump, Clark W. Barrett, and David L. Dill. CVC: A cooperating validity checker. In Int'l Conf. Computer Aided Verification (CAV '02), pages 500--504, 2002.
[41]
Andrew Tolmach and Dino P. Oliva. From ML to Ada: Strongly-typed language interoperability via source translation. J. Functional Programming, 8(4):367--412, 1998.
[42]
Hongwei Xi. Applied Type System (extended abstract). In TYPES 2003, LNCS, pages 394--408. Springer, 2004.
[43]
Hongwei Xi. Dependent types in practical programming. PhD thesis, Carnegie Mellon University, 1998.
[44]
Hongwei Xi and Frank Pfenning. Dependent types in practical programming. In POPL, pages 214--227, 1999.
[45]
Hongwei Xi, Chiyan Chen, and Gang Chen. Guarded recursive datatype constructors. In POPL, pages 224--235, 2003.

Cited By

View all

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
PLPV '07: Proceedings of the 2007 workshop on Programming languages meets program verification
October 2007
76 pages
ISBN:9781595936776
DOI:10.1145/1292597
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: 02 October 2007

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. dependent types
  2. intersection types
  3. type refinements
  4. union types

Qualifiers

  • Article

Conference

ICFP07
Sponsor:

Acceptance Rates

PLPV '07 Paper Acceptance Rate 6 of 8 submissions, 75%;
Overall Acceptance Rate 18 of 25 submissions, 72%

Upcoming Conference

POPL '26

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)6
  • Downloads (Last 6 weeks)0
Reflects downloads up to 14 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2024)Refinement Type RefutationsProceedings of the ACM on Programming Languages10.1145/36897458:OOPSLA2(962-987)Online publication date: 8-Oct-2024
  • (2023)Focusing on Refinement TypingACM Transactions on Programming Languages and Systems10.1145/361040845:4(1-62)Online publication date: 20-Dec-2023
  • (2022)Embedded Domain Specific VerifiersPrinciples of Systems Design10.1007/978-3-031-22337-2_26(535-553)Online publication date: 29-Dec-2022
  • (2021)Intensional datatype refinement: with application to scalable verification of pattern-match safetyProceedings of the ACM on Programming Languages10.1145/34343365:POPL(1-29)Online publication date: 4-Jan-2021
  • (2020)Resolution as intersection subtyping via Modus PonensProceedings of the ACM on Programming Languages10.1145/34282744:OOPSLA(1-30)Online publication date: 13-Nov-2020
  • (2019)Sound and complete bidirectional typechecking for higher-rank polymorphism with existentials and indexed typesProceedings of the ACM on Programming Languages10.1145/32903223:POPL(1-28)Online publication date: 2-Jan-2019
  • (2019)Manifest Contracts with Intersection TypesProgramming Languages and Systems10.1007/978-3-030-34175-6_3(33-52)Online publication date: 18-Nov-2019
  • (2018)Safe stream-based programming with refinement typesProceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering10.1145/3238147.3238174(565-576)Online publication date: 3-Sep-2018
  • (2017)Local refinement typingProceedings of the ACM on Programming Languages10.1145/31102701:ICFP(1-27)Online publication date: 29-Aug-2017
  • (2017)Extensible Datasort RefinementsProgramming Languages and Systems10.1007/978-3-662-54434-1_18(476-503)Online publication date: 19-Mar-2017
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media