{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,22]],"date-time":"2025-05-22T04:36:44Z","timestamp":1747888604715,"version":"3.41.0"},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662466773"},{"type":"electronic","value":"9783662466780"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46678-0_9","type":"book-chapter","created":{"date-parts":[[2015,4,1]],"date-time":"2015-04-01T13:42:21Z","timestamp":1427895741000},"page":"133-147","source":"Crossref","is-referenced-by-count":4,"title":["Sequent Calculus in the Topos of Trees"],"prefix":"10.1007","author":[{"given":"Ranald","family":"Clouston","sequence":"first","affiliation":[]},{"given":"Rajeev","family":"Gor\u00e9","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"doi-asserted-by":"crossref","unstructured":"Appel, A.W., Melli\u00e8s, P.A., Richards, C.D., Vouillon, J.: A very modal model of a modern, major, general type system. In: POPL, pp. 109\u2013122 (2007)","key":"9_CR1","DOI":"10.1145\/1190215.1190235"},{"key":"9_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-642-22863-6_5","volume-title":"Interactive Theorem Proving","author":"J. Bengtson","year":"2011","unstructured":"Bengtson, J., Jensen, J.B., Sieczkowski, F., Birkedal, L.: Verifying object-oriented programs with higher-order separation logic in Coq. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol.\u00a06898, pp. 22\u201338. Springer, Heidelberg (2011)"},{"doi-asserted-by":"crossref","unstructured":"Birkedal, L., M\u00f8gelberg, R.E.: Intensional type theory with guarded recursive types qua fixed points on universes. In: LICS, pp. 213\u2013222 (2013)","key":"9_CR3","DOI":"10.1109\/LICS.2013.27"},{"doi-asserted-by":"crossref","unstructured":"Birkedal, L., M\u00f8gelberg, R.E., Schwinghammer, J., St\u00f8vring, K.: First steps in synthetic guarded domain theory: Step-indexing in the topos of trees. LMCS\u00a08(4) (2012)","key":"9_CR4","DOI":"10.2168\/LMCS-8(4:1)2012"},{"unstructured":"Birkedal, L., Schwinghammer, J., St\u00f8vring, K.: A metric model of lambda calculus with guarded recursion. In: FICS, pp. 19\u201325 (2010)","key":"9_CR5"},{"key":"9_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-319-08918-8_8","volume-title":"Rewriting and Typed Lambda Calculi","author":"A. Bizjak","year":"2014","unstructured":"Bizjak, A., Birkedal, L., Miculan, M.: A model of countable nondeterminism in guarded type theory. In: Dowek, G. (ed.) RTA-TLCA 2014. LNCS, vol.\u00a08560, pp. 108\u2013123. Springer, Heidelberg (2014)"},{"doi-asserted-by":"crossref","unstructured":"Boolos, G.: The logic of provability. CUP (1995)","key":"9_CR7","DOI":"10.1017\/CBO9780511625183"},{"doi-asserted-by":"crossref","unstructured":"Chagrov, A., Zakharyaschev, M.: Modal Logic. OUP (1997)","key":"9_CR8","DOI":"10.1093\/oso\/9780198537793.001.0001"},{"key":"9_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"407","DOI":"10.1007\/978-3-662-46678-0_26","volume-title":"FoSSaCS 2015","author":"R. Clouston","year":"2015","unstructured":"Clouston, R., Bizjak, A., Grathwohl, H.B., Birkedal, L.: Programming and reasoning with guarded recursion for coinductive types. In: Pitts, A. (ed.) FoSSaCS 2015. LNCS, vol.\u00a09034, pp. 407\u2013421. Springer, Heidelberg (2015)"},{"doi-asserted-by":"crossref","unstructured":"Clouston, R., Gor\u00e9, R.: Sequent calculus in the topos of trees. arXiv:1501.03293, extended version (2015)","key":"9_CR10","DOI":"10.1007\/978-3-662-46678-0_9"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/3-540-58085-9_72","volume-title":"Types for Proofs and Programs","author":"T. Coquand","year":"1994","unstructured":"Coquand, T.: Infinite objects in type theory. In: Barendregt, H., Nipkow, T. (eds.) TYPES 1993. LNCS, vol.\u00a0806, pp. 62\u201378. Springer, Heidelberg (1994)"},{"issue":"2","key":"9_CR12","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/BF00373275","volume":"45","author":"G. Corsi","year":"1986","unstructured":"Corsi, G.: Semantic trees for Dummett\u2019s logic LC. Stud. Log.\u00a045(2), 199\u2013206 (1986)","journal-title":"Stud. Log."},{"doi-asserted-by":"crossref","unstructured":"Dreyer, D., Ahmed, A., Birkedal, L.: Logical step-indexed logical relations. In: LICS, pp. 71\u201380 (2009)","key":"9_CR13","DOI":"10.1109\/LICS.2009.34"},{"issue":"1-2","key":"9_CR14","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/s00153-011-0254-7","volume":"51","author":"R. Dyckhoff","year":"2012","unstructured":"Dyckhoff, R., Negri, S.: Proof analysis in intermediate logics. Arch. Math. Log.\u00a051(1-2), 71\u201392 (2012)","journal-title":"Arch. Math. Log."},{"issue":"2","key":"9_CR15","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/s10817-012-9252-7","volume":"51","author":"M. Ferrari","year":"2013","unstructured":"Ferrari, M., Fiorentini, C., Fiorino, G.: Contraction-free linear depth sequent calculi for intuitionistic propositional logic with the subformula property and minimal depth counter-models. J. Autom. Reason.\u00a051(2), 129\u2013149 (2013)","journal-title":"J. Autom. Reason."},{"issue":"1","key":"9_CR16","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/s10817-013-9276-7","volume":"52","author":"G. Fiorino","year":"2014","unstructured":"Fiorino, G.: Terminating calculi for propositional Dummett logic with subformula property. J. Autom. Reason.\u00a052(1), 67\u201397 (2014)","journal-title":"J. Autom. Reason."},{"doi-asserted-by":"crossref","unstructured":"Garg, D., Genovese, V., Negri, S.: Countermodels from sequent calculi in multi-modal logics. In: LICS, pp. 315\u2013324 (2012)","key":"9_CR17","DOI":"10.1109\/LICS.2012.42"},{"key":"9_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-642-29822-6_14","volume-title":"Functional and Logic Programming","author":"Y. Hirai","year":"2012","unstructured":"Hirai, Y.: A lambda calculus for G\u00f6del\u2013Dummett logic capturing waitfreedom. In: Schrijvers, T., Thiemann, P. (eds.) FLOPS 2012. LNCS, vol.\u00a07294, pp. 151\u2013165. Springer, Heidelberg (2012)"},{"key":"9_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/978-3-540-78739-6_27","volume-title":"Programming Languages and Systems","author":"A. Hobor","year":"2008","unstructured":"Hobor, A., Appel, A.W., Nardelli, F.Z.: Oracle semantics for concurrent separation logic. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol.\u00a04960, pp. 353\u2013367. Springer, Heidelberg (2008)"},{"key":"9_CR20","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-540-73099-6_13","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"R. Ishigaki","year":"2007","unstructured":"Ishigaki, R., Kikuchi, K.: Tree-sequent methods for subintuitionistic predicate logics. In: Olivetti, N. (ed.) TABLEAUX 2007. LNCS (LNAI), vol.\u00a04548, pp. 149\u2013164. Springer, Heidelberg (2007)"},{"doi-asserted-by":"crossref","unstructured":"Krishnaswami, N.R., Benton, N.: A semantic model for graphical user interfaces. In: ICFP, pp. 45\u201357 (2011)","key":"9_CR21","DOI":"10.1145\/2034574.2034782"},{"doi-asserted-by":"crossref","unstructured":"Krishnaswami, N.R., Benton, N.: Ultrametric semantics of reactive programs. In: LICS, pp. 257\u2013266 (2011)","key":"9_CR22","DOI":"10.1109\/LICS.2011.38"},{"unstructured":"Litak, T.: A typing system for the modalized Heyting calculus. In: COS (2013)","key":"9_CR23"},{"doi-asserted-by":"crossref","unstructured":"Litak, T.: Constructive modalities with provability smack, author\u2019s cut v. 2.03 (2014) (retrieved from author\u2019s website)","key":"9_CR24","DOI":"10.1007\/978-94-017-8860-1_8"},{"doi-asserted-by":"crossref","unstructured":"Milius, S., Litak, T.: Guard your daggers and traces: On the equational properties of guarded (co-) recursion. arXiv:1309.0895 (2013)","key":"9_CR25","DOI":"10.4204\/EPTCS.126.6"},{"key":"9_CR26","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/978-94-017-8860-1_7","volume":"4","author":"A. Muravitsky","year":"2014","unstructured":"Muravitsky, A.: Logic KM: A biography. Outstanding Contributions to Logic\u00a04, 155\u2013185 (2014)","journal-title":"Outstanding Contributions to Logic"},{"doi-asserted-by":"crossref","unstructured":"Nakano, H.: A modality for recursion. In: LICS, pp. 255\u2013266 (2000)","key":"9_CR27","DOI":"10.1109\/LICS.2000.855774"},{"doi-asserted-by":"crossref","unstructured":"Pottier, F.: A typed store-passing translation for general references. In: POPL, pp. 147\u2013158 (2011)","key":"9_CR28","DOI":"10.1145\/1925844.1926403"},{"issue":"1","key":"9_CR29","first-page":"116","volume":"34","author":"G. Restall","year":"1994","unstructured":"Restall, G.: Subintuitionistic logics. NDJFL\u00a034(1), 116\u2013129 (1994)","journal-title":"NDJFL"},{"unstructured":"Rowe, R.N.: Semantic Types for Class-based Objects. Ph.D. thesis, Imperial College London (2012)","key":"9_CR30"},{"key":"9_CR31","first-page":"7","volume":"7","author":"O. Sonobe","year":"1975","unstructured":"Sonobe, O.: A Gentzen-type formulation of some intermediate propositional logics. J. Tsuda College\u00a07, 7\u201314 (1975)","journal-title":"J. Tsuda College"},{"unstructured":"Troelstra, A., Schwichtenberg, H.: Basic Proof Theory. CUP (1996)","key":"9_CR32"},{"doi-asserted-by":"crossref","unstructured":"Wolter, F., Zakharyaschev, M.: Intuitionistic modal logics. In: Logic and Foundations of Mathematics, pp. 227\u2013238 (1999)","key":"9_CR33","DOI":"10.1007\/978-94-017-2109-7_17"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46678-0_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T19:57:38Z","timestamp":1747857458000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46678-0_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662466773","9783662466780"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46678-0_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}