Skip navigation
Skip navigation

Sequent Calculus in the Topos of Trees

Clouston, Ranald; Gore, Rajeev

Description

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
URI: http://hdl.handle.net/1885/67552
Source: Lecture Notes in Computer Science (LNCS)
DOI: 10.1007/978-3-662-46678-0_9

Download

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:  20 July 2017/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator