An Effective Theory of Type Refinements
Report ID: TR-656-02Author: Harper, Robert / Walker, David / Mandelbaum, Yitzhak
Date: 2002-12-00
Pages: 59
Download Formats: |PDF| |Postscript|
Abstract:
We develop an explicit two-level system that allows programmers to reason about the behavior of effectful programs. The first level is an ordinary ML-style type system, which confers standard properties on program behavior. The second level is a conservative extension of the first which uses a logic of type refinements to check more precise properties of program behavior. Our logic is a fragment of intuitionistic linear logic, which allows us the ability to reason locally about changes of program state. We provide a generic resource semantics for our logic as well as a sound, decidable syntactic refinement checking system. We also prove that refinements give rise to an optimization principle for programs. Finally, we illustrate the power of our system through a number of examples.