Computer Science Department
School of Computer Science, Carnegie Mellon University
A Bidirectional Refinement Type System for LF
William Lovas, Frank Pfenning
May 2008
This document is an extended version of a paper originally presented
at the
Second International Workshop on Logical Frameworks and
Meta-Languages:
Theory and Practice (LFMTP'07)
and published
in Electronic Notes in Theoretical Computer Science [LP08].
It supercedes Computer Science Technical Report CMU-CS-07-127,
which was unpublished.
We present a system of refinement types for LF in the style of recent formulations where only canonical forms are well-typed. Both the usual LF rules and the rules for type refinements are bidirectional, leading to a straightforward proof of decidability of typechecking even in the presence of intersection types. Because we insist on canonical forms, structural rules for subtyping can now be derived rather than being assumed as primitive. We illustrate the expressive power of our system with several examples in the domain of logics and programming languages.
58 pages
Return to:
SCS Technical Report Collection This page maintained by reports@cs.cmu.edu
School of Computer Science