William Lovas

Thesis Title: Refinement Types for Logical Frameworks
Degree Type: Ph.D. in Computer Science
Advisor(s): Frank Pfenning
Graduated: December 2010

Abstract:

The logical framework LF and its metalogic Twelf can be used to encode and reason about a wide variety of logics, languages, and other deductive systems in a formal, machine-checkable way.

Recent studies have shown that ML-like languages can profitably be extended with a notion of subtyping called refinement types. A refinement type discipline uses an extra layer of term classification above the usual type system to more accurately capture certain properties of terms.

I propose that adding refinement types to LF is both useful and practical. To support the claim, I exhibit an extension of LF with refinement types called LFR,work out important details of its metatheory, delineate a practical algorithm for refinement type reconstruction, and present several case studies that highlight the utility of refinement types for formalized mathematics. In the end I find that refinement types and LF are a match made in heaven: refinements enable many rich new modes of expression, and the simplicity of LF ensures that they come at a modest cost.

Thesis Committee:
Frank Pfenning, (Chair)
Karl Crary
Robert Harper
Adriana Compagnoni (Stevens)
Carsten Schürmann (ITU Copenhagen)

Jeannette Wing, Head, Computer Science Department
Randy Bryant, Dean, School of Computer Science

Keywords:
Refinement types, logical frameworks, subtyping, intersection types, dependent types