Skip navigation
Skip navigation

Sequent Calculus in the Topos of Trees

Clouston, Ranald; Gore, Rajeev


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

CollectionsANU Research Publications
Date published: 2015
Type: Journal article
Source: Lecture Notes in Computer Science (LNCS)
DOI: 10.1007/978-3-662-46678-0_9


File Description SizeFormat Image
01_Clouston_Sequent_Calculus_in_the_Topos_2015.pdf282.07 kBAdobe PDF    Request a copy

Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  19 May 2020/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator