Carnegie Mellon University
Browse
Refinement Types for Logical Frameworks.pdf (1.33 MB)

Refinement Types for Logical Frameworks

Download (1.33 MB)
thesis
posted on 2010-09-01, 00:00 authored by William Lovas

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 itsmetatheory, delineate a practical algorithmfor refinement type reconstruction, andpresent 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.

History

Date

2010-09-01

Degree Type

  • Dissertation

Department

  • Computer Science

Degree Name

  • Doctor of Philosophy (PhD)

Advisor(s)

Frank Pfenning,Karl Crary,Robert Harper,Adriana Compagnoni,Carsten Schurmann

Usage metrics

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC