Sequent Calculus in the Topos of Trees

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

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
  • References (32)
    32 references, page 1 of 4

    1. Appel, A.W., Melli`es, P.A., Richards, C.D., Vouillon, J.: A very modal model of a modern, major, general type system. In: POPL. pp. 109-122 (2007)

    2. Bengtson, J., Jensen, J.B., Sieczkowski, F., Birkedal, L.: Verifying object-oriented programs with higher-order separation logic in Coq. In: ITP, pp. 22-38 (2011)

    3. Birkedal, L., Møgelberg, R.E.: Intensional type theory with guarded recursive types qua fixed points on universes. In: LICS. pp. 213-222 (2013)

    4. Birkedal, L., Møgelberg, R.E., Schwinghammer, J., Støvring, K.: First steps in synthetic guarded domain theory: step-indexing in the topos of trees. LMCS 8(4) (2012)

    5. Birkedal, L., Schwinghammer, J., Støvring, K.: A metric model of lambda calculus with guarded recursion. In: FICS. pp. 19-25 (2010)

    6. Bizjak, A., Birkedal, L., Miculan, M.: A model of countable nondeterminism in guarded type theory. In: RTA-TLCA. pp. 108-123 (2014)

    7. Boolos, G.: The logic of provability. CUP (1995)

    8. Chagrov, A., Zakharyaschev, M.: Modal Logic. OUP (1997)

    9. Clouston, R., Bizjak, A., Grathwohl, H.B., Birkedal, L.: Programming and reasoning with guarded recursion for coinductive types. In: FoSSaCS (2015)

    10. Coquand, T.: Infinite objects in type theory. In: TYPES. pp. 62-78 (1993)

  • Metrics
    No metrics available
Share - Bookmark