Sequent Calculus in the Topos of Trees

Loading...
Thumbnail Image

Date

Authors

Clouston, Ranald
Gore, Rajeev

Journal Title

Journal ISSN

Volume Title

Publisher

Springer

Abstract

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

Description

Keywords

Citation

Source

Lecture Notes in Computer Science (LNCS)

Book Title

Entity type

Access Statement

License Rights

Restricted until

2037-12-31