Refinement types for ML
- 1 May 1991
- journal article
- Published by Association for Computing Machinery (ACM) in ACM SIGPLAN Notices
- Vol. 26 (6) , 268-277
- https://doi.org/10.1145/113446.113468
Abstract
T$’e describe a refinement of ML’s type system allowing the specification of recursively defined subtypes of user-defined datatypes. The resulting system of rejirzemeni f,ypes preserves desirable properties of ML such as decidability of type inference, while at the same time allowing more errors to be detected at compile-time. The type system combines abstract interpretation with ideas from the intersection type discipline, but remains closely tied to ML in that refinement types are given only to programs which are already well-typed in ML.Keywords
This publication has 7 references indexed in Scilit:
- A decision procedure for a class of set constraintsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Type reconstruction in the presence of polymorphic recursionACM Transactions on Programming Languages and Systems, 1993
- F-bounded polymorphism for object-oriented programmingPublished by Association for Computing Machinery (ACM) ,1989
- Principal type scheme and unification for intersection type disciplineTheoretical Computer Science, 1988
- Graph-Based Algorithms for Boolean Function ManipulationIEEE Transactions on Computers, 1986
- A simple applicative language: mini-MLPublished by Association for Computing Machinery (ACM) ,1986
- On understanding types, data abstraction, and polymorphismACM Computing Surveys, 1985