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
and published in Electronic Notes in Theoretical Computer Science [LP08].
It supercedes Computer Science Technical Report CMU-CS-07-127, which was unpublished.


Keywords: LF, refinement types, subtyping, dependent types, intersection types

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
School of Computer Science

This page maintained by