An Effective Theory of Type Refinements

Yitzhak Mandelbaum, David Walker, Robert Harper

Research output: Contribution to conferencePaper

30 Scopus citations


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 that uses a logic of type refinements to check more precise properties of program behavior. Our logic is a fragment of intuitionistic linear logic, which gives programmers 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.

Original languageEnglish (US)
Number of pages13
StatePublished - 2003
EventEighth ACM SIGPLAN International Conference on Functional Programming - Uppsala, Sweden
Duration: Aug 25 2003Aug 29 2003


OtherEighth ACM SIGPLAN International Conference on Functional Programming

All Science Journal Classification (ASJC) codes

  • Software


  • Effectful Computation
  • Linear Logic
  • Local Reasoning
  • Type Refinement
  • Type Theory

Fingerprint Dive into the research topics of 'An Effective Theory of Type Refinements'. Together they form a unique fingerprint.

  • Cite this

    Mandelbaum, Y., Walker, D., & Harper, R. (2003). An Effective Theory of Type Refinements. 213-225. Paper presented at Eighth ACM SIGPLAN International Conference on Functional Programming, Uppsala, Sweden.