Sequent Calculus in the Topos of Trees

Contribution for newspaper or weekly magazine, Preprint English OPEN
Clouston, Ranald; Goré, Rajeev;
(2015)
  • Publisher: Springer VS
  • Related identifiers: doi: 10.1007/978-3-662-46678-0_9
  • Subject: Computer Science - Logic in Computer Science
    acm: TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES | TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS

Nakano's "later" modality, inspired by G\"{o}del-L\"{o}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 the semantics o... View more
Share - Bookmark