Doctoral Thesis Proposal - Zhibo Chen
April 20, 2026 1:00PM—2:30PM
Location:
In Person
-
Gates Hillman 5117
Speaker:
ZHIBO CHEN,
Ph.D. Student
Computer Science Department
Carnegie Mellon University
https://www.andrew.cmu.edu/user/zhiboc/
The LF logical framework represents judgments as types, and objects and derivations as finitary terms. Twelf, an implementation of LF, is a metalogical framework that incorporates metatheorem checking and a logic programming engine. There is no direct encoding of infinitary objects and derivations in LF and Twelf. In this thesis, we propose a new logical framework CoLF, building on top of LF, for encoding infinitary objects and derivations as infinitary terms. We develop the type theory and implementation of CoLF. We also propose to investigate the metatheoretic reasoning principles and a new logic programming semantics in the presence of infinitary terms.
Thesis Committee
Frank Pfenning (Chair)
Karl Crary
Iliano Cervesato
Alberto Momigliano (University of Milan)
Additional Information
For More Information:
matthewstewart@cmu.edu