Frame Type Theory


Writing modular programs in proof assistants is notoriously difficult. A significant literature and implementation effort is devoted to the topic, with approaches ranging from adding new constructions to the underlying logic, to adding features to the proof assistant. However, all current options (including records, sections and modules) are unsatisfactory in one way or another. In this work (in progress), we aim at reconciling the pros of several options using frames.

Thu, Jun 13, 2019 11:00 — 11:15
Ingeniørenes Hus Møtesenter
Kronprinsens gate 17
0251 Oslo
PhD student