Sequent Calculus in the Topos of Trees
Nakano’s “later” modality, inspired by Gödel-Löb provability logic, has been applied in type systems and program logics to capture guarded recursion. Birkedal et al modelled this modality via the internal logic of the topos of trees. We show that
|Collections||ANU Research Publications|
|Source:||Lecture Notes in Computer Science (LNCS)|
|01_Clouston_Sequent_Calculus_in_the_Topos_2015.pdf||282.07 kB||Adobe PDF||Request a copy|
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.