Frame Type Theory

Abstract

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.

Date
Thu, Jun 13, 2019 11:00 — 11:15
Location
Ingeniørenes Hus Møtesenter
Kronprinsens gate 17<br>0251 Oslo