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.
| Identifer | oai:union.ndltd.org:cmu.edu/oai:repository.cmu.edu:dissertations-1066 |
| Date | 01 September 2010 |
| Creators | Lovas, William |
| Publisher | Research Showcase @ CMU |
| Source Sets | Carnegie Mellon University |
| Detected Language | English |
| Type | text |
| Format | application/pdf |
| Source | Dissertations |
Page generated in 0.002 seconds