When: Wednesday, May 21, 10:30 a.m.

Where: 4615A Wean Hall

William Lovas

Thesis Proposal

Abstract:
The logical framework LF and its implementation as the Twelf metalogic provide both a practical system and a proven methodology for representing deductive systems and their metatheory in a machine-checkable way. An extension of LF with refinement types provides a convenient means for representing certain kinds of judgemental inclusions in an intrinsic manner. I propose to carry out such an extension in full, adapting as much of the Twelf metatheory engine as possible to the new system, and I intend to argue that the extension is both useful and practical.

Thesis Committee:
Frank Pfenning, Chair
Robert Harper
Karl Crary
Adriana Compagnoni, Stevens Institute of Technology
Carsten Schuermann, IT University Copenhagen

Thesis Summary: http://www.cs.cmu.edu/~lovas/papers/proposal.pdf

<< Back