An effective theory of type refinements

Yitzhak Mandelbaum, David Walker, Robert Harper

Research output: Contribution to journalConference articlepeer-review

19 Scopus citations

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 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)
Pages (from-to)213-225
Number of pages13
JournalACM SIGPLAN Notices
Volume38
Issue number9
DOIs
StatePublished - Sep 2003
EventProceedings of the 2003 ACM SIGPLAN International Conference on Functional Programming - Uppsala, Sweden
Duration: Aug 25 2003Aug 29 2003

All Science Journal Classification (ASJC) codes

  • Software
  • Computer Graphics and Computer-Aided Design

Keywords

  • 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