Article

Free access

Refinement types for ML

Authors:

Tim Freeman,

Frank PfenningAuthors Info & Claims

PLDI '91: Proceedings of the ACM SIGPLAN 1991 conference on Programming language design and implementation

Pages 268 - 277

https://doi.org/10.1145/113445.113468

Published: 01 May 1991 Publication History

PDF eReader

References

[1]

Roberto M. Amadio and Luca Cardelli. Subtyping recursive types. Research Report 62, Digital Systems Research Center, Palo Alto, California, August 1990.

Google Scholar

[2]

J. R. Butch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. In Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, pages 428-439, Philadelphia, PA, June 1990. IEEE Computer Society Press.

Google Scholar

[3]

Randal E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677- 691, August 1986.

Digital Library

Google Scholar

[4]

Luca Cardelli. Typeful programming. Research Report 45, Digital Equipment Corporation, Systems Research Center, Palo Alto, California, February 1989.

Google Scholar

[5]

Peter Canning, William Cook, Waiter Hill, and Waiter Olthoff. F-bounded polymorphism for object-oriented programming. In Functional Programming Languages and Computer Avchztectuve. ACM, 1989.

Digital Library

Google Scholar

[6]

Dominique Clement, Jo{lle Despeyroux, Thierry Despeyroux, and Gilles Kahn. A simple applicative language: Mini-ML. In Proceedings of the 1986 Conference on LISP and Functional Programming. ACM Press, 1986.

Digital Library

Google Scholar

[7]

Luca Cardelli and Peter Wether. On understanding types, data abstraction, and polymorphism. A CM Computing Surveys, 17:471-522, 1985.

Digital Library

Google Scholar

[8]

Ferenc G~cseg and Magnus Steinby. Tree Automata. Akad~miai Kiad6, Budapest, 1984.

Google Scholar

[9]

Nevin Heintze and Joxan Jaffar. A decision procedure for a class of set constraints. In Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, Ph,ladelphia. IEEE, June 1990.

Crossref

Google Scholar

[10]

A.J. Kfoury, J. Tiuryn, and P. Urzyczyn. Type-checking in the presence of polymorphic recursion. To appear in TOPLA$, October 1989.

Digital Library

Google Scholar

[11]

Prateek Mishra. Towards a theory of types in Prolog. In Irttevnational Symposium on Logic Programming, pages 289-298. IEEE, 1984.

Google Scholar

[12]

Robin Milner, Mads Torte, and Robert Harper. The Defimiior~ of S~andard ML. MIT Press, Cambridge, Massachusetts, 1990.

Digital Library

Google Scholar

[13]

Alan Mycroft. Polymorphic Type Schemes and Recuvsive Definitions, pages 217-228. International Symposium on Programming. Springer-Verlag, New York, 1984. LNCS 167.

Digital Library

Google Scholar

[14]

Benjamin Pierce. A decision procedure for the subtype relation on intersection types with bounded variables. Technical Report CMU-CS-89-169, School of Computer Science, Carnegie Mellon University, Pittsburgh, Pennsylvania, September 1989.

Google Scholar

[15]

Benjamin C. Pierce. Preliminary investigation of a calculus with intersection and union types. Unpublished manuscript, June 1990.

Google Scholar

[16]

Simone Ronchi Della Rocca. Principal type scheme and unification for intersection type discipline. Theoretical Computer Science, 59:181-209, 1988.

Digital Library

Google Scholar

[17]

John C. Reynolds. Preliminary design of the programming language Forsythe. Technical Report CMU-CS-88-159, Carnegie Mellon University, Pittsburgh, Pennsylvania, June 1988.

Google Scholar

[18]

Eyal Yardeni, Thorn Fruehwirth, and Ehud Shapiro. Polymorphically typed logic programs. In Frank Pfenning, editor, Types in Logic Programming. MIT Press, Cambridge, Massachusetts, 1991. To appear.

Google Scholar

Cited By

View all

Rehman BOliveira BDi Stefano L(2024)Disjoint Polymorphism with Intersection and Union TypesProceedings of the 26th ACM International Workshop on Formal Techniques for Java-like Programs10.1145/3678721.3686230(23-29)Online publication date: 20-Sep-2024
https://dl.acm.org/doi/10.1145/3678721.3686230
van Brügge JVazou NMorris J(2024)Liquid Amortization: Proving Amortized Complexity with LiquidHaskell (Functional Pearl)Proceedings of the 17th ACM SIGPLAN International Haskell Symposium10.1145/3677999.3678282(97-108)Online publication date: 29-Aug-2024
https://dl.acm.org/doi/10.1145/3677999.3678282
Kawamata FUnno HSekiyama TTerauchi T(2024)Answer Refinement Modification: Refinement Type System for Algebraic Effects and HandlersProceedings of the ACM on Programming Languages10.1145/36332808:POPL(115-147)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3633280
Show More Cited By

Index Terms

Refinement types for ML
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
        Data types and structures
      2. Language types
2. Theory of computation
  1. Semantics and reasoning
    1. Program constructs
      1. Functional constructs
      2. Type structures

Recommendations

Quality Meshing with Weighted Delaunay Refinement

Delaunay meshes with bounded circumradius to shortest edge length ratio have been proposed in the past for quality meshing. The only poor quality tetrahedra, called slivers, that can occur in such a mesh can be eliminated by the sliver exudation ...
Adaptive mesh refinement for conformal hexahedralmeshes

In a numerical simulation using the finite element method, the mesh has to be fine enough to guarantee the accuracy of the solution. However, a uniformly fine mesh will usually imply a more expensive computation. Mesh adaptation offers an effective ...
Delaunay refinement mesh generation

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

PLDI '91: Proceedings of the ACM SIGPLAN 1991 conference on Programming language design and implementation

May 1991

356 pages

ISBN:0897914287

DOI:10.1145/113445

Chairman:
David S. Wise
Indiana Univ., Bloomington

ACM SIGPLAN Notices Volume 26, Issue 6
June 1991
352 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/113446
Editor:
Richard L. Wexelblat
IDA/CSED, Alexandria, VA
Issue’s Table of Contents

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: 01 May 1991

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

PLDI91

Sponsor:

SIGPLAN

PLDI91: Conference on Programming Languages Design and Implementation

June 24 - 28, 1991

Ontario, Toronto, Canada

Acceptance Rates

Overall Acceptance Rate 406 of 2,067 submissions, 20%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

341
Total Citations
View Citations
2,000
Total Downloads

Downloads (Last 12 months)372
Downloads (Last 6 weeks)52

Reflects downloads up to 23 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Rehman BOliveira BDi Stefano L(2024)Disjoint Polymorphism with Intersection and Union TypesProceedings of the 26th ACM International Workshop on Formal Techniques for Java-like Programs10.1145/3678721.3686230(23-29)Online publication date: 20-Sep-2024
https://dl.acm.org/doi/10.1145/3678721.3686230
van Brügge JVazou NMorris J(2024)Liquid Amortization: Proving Amortized Complexity with LiquidHaskell (Functional Pearl)Proceedings of the 17th ACM SIGPLAN International Haskell Symposium10.1145/3677999.3678282(97-108)Online publication date: 29-Aug-2024
https://dl.acm.org/doi/10.1145/3677999.3678282
Kawamata FUnno HSekiyama TTerauchi T(2024)Answer Refinement Modification: Refinement Type System for Algebraic Effects and HandlersProceedings of the ACM on Programming Languages10.1145/36332808:POPL(115-147)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3633280
DeYoung HMordido APfenning FDas A(2024)Parametric Subtyping for Structural Parametric PolymorphismProceedings of the ACM on Programming Languages10.1145/36329328:POPL(2700-2730)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632932
Elsman M(2024)Explicit Effects and Effect Constraints in ReMLProceedings of the ACM on Programming Languages10.1145/36329218:POPL(2370-2394)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632921
Hwang SLee SRyu S(2024)An Empirical Study of JVMs’ Behaviors on Erroneous JNI InteroperationsIEEE Transactions on Software Engineering10.1109/TSE.2024.337323950:4(979-994)Online publication date: Apr-2024
https://doi.org/10.1109/TSE.2024.3373239
Xu M(2024)Research Report: Not All Move Specifications Are Created Equal : A Case Study on the Formally Verified Diem Payment Network2024 IEEE Security and Privacy Workshops (SPW)10.1109/SPW63631.2024.00024(200-214)Online publication date: 23-May-2024
https://doi.org/10.1109/SPW63631.2024.00024
Colledan ADal Lago U(2024)Circuit Width Estimation via Effect Typing and Linear DependencyProgramming Languages and Systems10.1007/978-3-031-57267-8_1(3-30)Online publication date: 5-Apr-2024
https://doi.org/10.1007/978-3-031-57267-8_1
Gavazzo FTreglia RVanoni G(2024)Monadic Intersection Types, RelationallyProgramming Languages and Systems10.1007/978-3-031-57262-3_2(22-51)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57262-3_2
Gaulin APientka B(2023)Contextual Refinement TypesElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.396.2396(4-19)Online publication date: 17-Nov-2023
https://doi.org/10.4204/EPTCS.396.2
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Get Access

Login options

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

Cited By

Index Terms

Recommendations

Quality Meshing with Weighted Delaunay Refinement

Adaptive mesh refinement for conformal hexahedralmeshes

Delaunay refinement mesh generation