DID YOU KNOW? DTIC has over 3.5 million final reports on DoD funded research, development, test, and evaluation activities available to our registered users. Click
HERE to register or log in.
Accession Number:
ADA278937
Title:
Refinement Types ML
Descriptive Note:
Doctoral thesis
Corporate Author:
CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE
Report Date:
1994-03-16
Pagination or Media Count:
336.0
Abstract:
Programming computers is a notoriously error-prone process. It is the job of the programming language designer to make this process more reliable. One approach to this is to impose some sort of typing discipline on the programs. In doing this, the programming language designer is immediately faced with a tradeoff if the type system is too simple, it cannot accurately express important properties of the program if it is too expressive, then mechanically checking or inferring the types becomes impractical. This thesis describes a type system called refinement types, which is an example of a new way to make this tradeoff, as well as a potentially useful system in itself. Refinement type inference requires programs to have types in two type systems an expressive type inference system intersection types with subtyping and a relatively simple type system basic polymorphic type inference. Refinement type inference inherits some properties from each of these as in intersection types with subtyping, we can use the type system to do abstract interpretation as in basic polymorphic type inference, refinement type inference is decidable preliminary experiments suggest refinement type inference may be practical as well. We have implemented refinement type inference for a subset of Standard ML to test these ideas. We have added new syntax, called rectype declarations, to allow the programmer to specify relevant domains for the abstract interpretation.
Distribution Statement:
APPROVED FOR PUBLIC RELEASE
