{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T08:38:08Z","timestamp":1742978288747,"version":"3.40.3"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030452308"},{"type":"electronic","value":"9783030452315"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We describe a category-theoretic semantics for a simply typed variant of Cocon, a contextual modal type theory where the box modality mediates between the weak function space that is used to represent higher-order abstract syntax (HOAS) trees and the strong function space that describes (recursive) computations about them. What makes Cocon different from standard type theories is the presence of first-class contexts and contextual objects to describe syntax trees that are closed with respect to a given context of assumptions. Following M.\u00a0Hofmann\u2019s work, we use a presheaf model to characterise HOAS trees. Surprisingly, this model already provides the necessary structure to also model Cocon. In particular, we can capture the contextual objects of Cocon using a comonad\u00a0<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\flat $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mo>\u266d<\/mml:mo>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> that restricts presheaves to their closed elements. This gives a simple semantic characterisation of the invariants of contextual types (e.g.\u00a0substitution invariance) and identifies Cocon as a type-theoretic syntax of presheaf models. We express our category-theoretic constructions by using a modal internal type theory that is implemented in Agda-Flat.<\/jats:p>","DOI":"10.1007\/978-3-030-45231-5_26","type":"book-chapter","created":{"date-parts":[[2020,4,17]],"date-time":"2020-04-17T10:02:53Z","timestamp":1587117773000},"page":"502-521","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Semantical Analysis of Contextual Types"],"prefix":"10.1007","author":[{"given":"Brigitte","family":"Pientka","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ulrich","family":"Sch\u00f6pp","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,4,17]]},"reference":[{"key":"26_CR1","unstructured":"The Agda sources for this paper are available from: http:\/\/github.com\/uelis\/contextual."},{"key":"26_CR2","doi-asserted-by":"crossref","unstructured":"Guillaume Allais, Robert Atkey, James Chapman, Conor McBride, and James McKinna. A type and scope safe universe of syntaxes with binding: Their semantics and proofs. Proc. ACM Program. Lang., 2(ICFP):90:1\u201390:30, July 2018.","DOI":"10.1145\/3236785"},{"key":"26_CR3","doi-asserted-by":"crossref","unstructured":"Benton, P.N., Bierman, G.M., de\u00a0Paiva, V., Hyland, M.: A term calculus for intuitionistic linear logic. In: Bezem, M., Groote, J.F. (eds.) Typed Lambda Calculi and Applications, International Conference on Typed Lambda Calculi and Applications, TLCA \u201993, Utrecht, The Netherlands, March 16-18, 1993, Proceedings. vol.\u00a0664, pp. 75\u201390. Springer (1993)","DOI":"10.1007\/BFb0037099"},{"key":"26_CR4","unstructured":"Andrew Barber and Gordon Plotkin. Dual intuitionistic linear logic. Technical Report, LFCS, University of Edinburgh, 1997."},{"key":"26_CR5","doi-asserted-by":"crossref","unstructured":"John Cartmell. Generalised algebraic theories and contextual categories. Annals of Pure and Applied Logic, 32:209 \u2013 243, 1986.","DOI":"10.1016\/0168-0072(86)90053-9"},{"key":"26_CR6","doi-asserted-by":"crossref","unstructured":"Rowan Davies and Frank Pfenning. A modal analysis of staged computation. Journal of the ACM, 48(3):555\u2013604, 2001.","DOI":"10.1145\/382780.382785"},{"key":"26_CR7","doi-asserted-by":"crossref","unstructured":"Peter Dybjer. Internal type theory. In Types for Proofs and Programs (TYPES\u201995), pages 120\u2013134, 1995.","DOI":"10.1007\/3-540-61780-9_66"},{"key":"26_CR8","unstructured":"M.\u00a0Fiore, G.\u00a0D. Plotkin, and D.\u00a0Turi. Abstract syntax and variable binding. In Logic in Computer Science (LICS\u201999), pages 193\u2013202. IEEE Press, 1999."},{"key":"26_CR9","unstructured":"Murdoch Gabbay and Andrew Pitts. A new approach to abstract syntax involving binders. In Logic in Computer Science (LICS\u201999), pages 214\u2013224. IEEE Press, 1999."},{"key":"26_CR10","doi-asserted-by":"crossref","unstructured":"Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the ACM, 40(1):143\u2013184, January 1993.","DOI":"10.1145\/138027.138060"},{"key":"26_CR11","doi-asserted-by":"crossref","unstructured":"Martin Hofmann. Syntax and Semantics of Dependent Types, page 79\u2013130. Publications of the Newton Institute. Cambridge University Press, 1997.","DOI":"10.1017\/CBO9780511526619.004"},{"key":"26_CR12","unstructured":"Martin Hofmann. Semantical analysis of higher-order abstract syntax. In Logic in Computer Science (LICS\u201999), pages 204\u2013213. IEEE Press, 1999."},{"key":"26_CR13","doi-asserted-by":"crossref","unstructured":"Furio Honsell, Marino Miculan, and Ivan Scagnetto. An axiomatic approach to metareasoning on nominal algebras in HOAS. In International Colloquium on Automata, Languages and Programming (ICALP\u201901), LNCS 2076, pages 963\u2013978. Springer, 2001.","DOI":"10.1007\/3-540-48224-5_78"},{"key":"26_CR14","doi-asserted-by":"crossref","unstructured":"Bart Jacobs. Comprehension categories and the semantics of type dependency. Theor. Comput. Sci., 107(2):169\u2013207, 1993.","DOI":"10.1016\/0304-3975(93)90169-T"},{"key":"26_CR15","unstructured":"Kavvos, G.A.: Intensionality, intensional recursion, and the G\u00f6del-L\u00f6b axiom. CoRR abs\/1703.01288 (2017), http:\/\/arxiv.org\/abs\/1703.01288"},{"key":"26_CR16","unstructured":"Daniel\u00a0R. Licata, Ian Orton, Andrew\u00a0M. Pitts, and Bas Spitters. Internal universes in models of homotopy type theory. In Formal Structures for Computation and Deduction (FSCD\u201918), pages 22:1\u201322:17, 2018."},{"key":"26_CR17","doi-asserted-by":"crossref","unstructured":"Dale Miller and Catuscia Palamidessi. Foundational aspects of syntax. ACM Comput. Surv., 31(3es), 1999.","DOI":"10.1145\/333580.333590"},{"key":"26_CR18","doi-asserted-by":"crossref","unstructured":"Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka. Contextual modal type theory. ACM Transactions on Computational Logic, 9(3):1\u201349, 2008.","DOI":"10.1145\/1352582.1352591"},{"key":"26_CR19","doi-asserted-by":"crossref","unstructured":"Frank Pfenning and Conal Elliott. Higher-order abstract syntax. In Symposium on Language Design and Implementation (PLDI\u201988), pages 199\u2013208, June 1988.","DOI":"10.1145\/960116.54010"},{"key":"26_CR20","doi-asserted-by":"crossref","unstructured":"Brigitte Pientka. A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions. In Principles of Programming Languages (POPL\u201908), pages 371\u2013382. ACM Press, 2008.","DOI":"10.1145\/1328897.1328483"},{"key":"26_CR21","unstructured":"Brigitte Pientka and Andreas Abel. Well-founded recursion over contextual objects. In Typed Lambda Calculi and Applications (TLCA\u201915), pages 273\u2013287, 2015."},{"key":"26_CR22","unstructured":"Brigitte Pientka, Andreas Abel, Francisco Ferreira, David Thibodeau, and R\u00e9becca Zucchini. Cocon: Computation in contextual type theory. CoRR, abs\/1901.03378, 2019."},{"key":"26_CR23","doi-asserted-by":"crossref","unstructured":"Brigitte Pientka, Andreas Abel, Francisco Ferreira, David Thibodeau, and Rebecca Zucchini. A type theory for defining logics and proofs. In 34th IEEE\/ ACM Symposium on Logic in Computer Science (LICS\u201919), pages 1\u201313, IEEE Computer Society, 2019.","DOI":"10.1109\/LICS.2019.8785683"},{"key":"26_CR24","doi-asserted-by":"crossref","unstructured":"Brigitte Pientka and Andrew Cave. Inductive Beluga: Programming Proofs (System Description). In Conference on Automated Deduction (CADE-25), LNCS 9195, pages 272\u2013281. Springer, 2015.","DOI":"10.1007\/978-3-319-21401-6_18"},{"key":"26_CR25","doi-asserted-by":"crossref","unstructured":"Brigitte Pientka and Joshua Dunfield. Programming with proofs and explicit contexts. In Principles and Practice of Declarative Programming (PPDP\u201908), pages 163\u2013173, 2008.","DOI":"10.1145\/1389449.1389469"},{"key":"26_CR26","doi-asserted-by":"crossref","unstructured":"Brigitte Pientka and Joshua Dunfield. Beluga: a framework for programming and reasoning with deductive systems (System Description). In International Joint Conference on Automated Reasoning (IJCAR\u201910), LNAI 6173, pages 15\u201321. Springer, 2010.","DOI":"10.1007\/978-3-642-14203-1_2"},{"key":"26_CR27","doi-asserted-by":"crossref","unstructured":"Shulman, M.: Brouwer\u2019s fixed-point theorem in real-cohesive homotopy type theory. Mathematical Structures in Computer Science 28(6), 856\u2013941 (2018)","DOI":"10.1017\/S0960129517000147"},{"key":"26_CR28","doi-asserted-by":"crossref","unstructured":"Thomas Streicher. Semantics of Type Theory. Birkh\u00e4user, 1991.","DOI":"10.1007\/978-1-4612-0433-6"},{"key":"26_CR29","unstructured":"Andrea Vezzosi. Agda with a flat modality. Available from https:\/\/github.com\/agda\/agda\/tree\/flat, 2018."}],"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-030-45231-5_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,1,7]],"date-time":"2021-01-07T14:00:24Z","timestamp":1610028024000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-45231-5_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030452308","9783030452315"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-45231-5_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"17 April 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FoSSaCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Dublin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Ireland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 April 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 April 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2020\/fossacs","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"98","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"31","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"32% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"12","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference could not take place due to the COVID-19 pandemic. There was an online event on July 2, 2020.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}