{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,17]],"date-time":"2025-10-17T13:46:46Z","timestamp":1760708806813,"version":"3.41.0"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"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_7","type":"book-chapter","created":{"date-parts":[[2015,4,1]],"date-time":"2015-04-01T13:42:21Z","timestamp":1427895741000},"page":"102-116","source":"Crossref","is-referenced-by-count":9,"title":["A Categorical Semantics for Linear Logical Frameworks"],"prefix":"10.1007","author":[{"given":"Matthijs","family":"V\u00e1k\u00e1r","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"7_CR1","first-page":"127","volume":"36","author":"P. Martin-L\u00f6f","year":"1998","unstructured":"Martin-L\u00f6f, P.: An intuitionistic theory of types. Twenty-five Years of Constructive Type Theory\u00a036, 127\u2013172 (1998)","journal-title":"Twenty-five Years of Constructive Type Theory"},{"issue":"1","key":"7_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J.Y. Girard","year":"1987","unstructured":"Girard, J.Y.: Linear logic. Theoretical Computer Science\u00a050(1), 1\u2013101 (1987)","journal-title":"Theoretical Computer Science"},{"key":"7_CR3","unstructured":"Program, T.U.F.: Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study (2013), http:\/\/homotopytypetheory.org\/book"},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"Cervesato, I., Pfenning, F.: A linear logical framework. In: LICS 1996. Proceedings, pp. 264\u2013275. IEEE (1996)","DOI":"10.1109\/LICS.1996.561339"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Dal\u00a0Lago, U., Gaboardi, M.: Linear dependent types and relative completeness. In: LiCS 2011. Proceeding, pp. 133\u2013142. IEEE (2011)","DOI":"10.1109\/LICS.2011.22"},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"Petit, B., et al.: Linear dependent types in a call-by-value scenario. In: Proceedings of the 14th Symposium on Principles and Practice of Declarative Programming, pp. 115\u2013126. ACM (2012)","DOI":"10.1145\/2370776.2370792"},{"key":"7_CR7","doi-asserted-by":"crossref","first-page":"357","DOI":"10.1145\/2480359.2429113","volume":"48","author":"M. Gaboardi","year":"2013","unstructured":"Gaboardi, M., Haeberlen, A., Hsu, J., Narayan, A., Pierce, B.C.: Linear dependent types for differential privacy. ACM SIGPLAN Notices\u00a048, 357\u2013370 (2013)","journal-title":"ACM SIGPLAN Notices"},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"Watkins, K., Cervesato, I., Pfenning, F., Walker, D.: A concurrent logical framework i: Judgments and properties. Technical report, DTIC Document (2003)","DOI":"10.21236\/ADA418517"},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"May, J.P., Sigurdsson, J.: Parametrized homotopy theory, vol.\u00a0132. American Mathematical Soc. (2006)","DOI":"10.1090\/surv\/132"},{"issue":"21","key":"7_CR10","first-page":"616","volume":"28","author":"M. Shulman","year":"2013","unstructured":"Shulman, M.: Enriched indexed categories. Theory and Applications of Categories\u00a028(21), 616\u2013695 (2013)","journal-title":"Theory and Applications of Categories"},{"issue":"23","key":"7_CR11","first-page":"582","volume":"26","author":"K. Ponto","year":"2012","unstructured":"Ponto, K., Shulman, M.: Duality and traces for indexed monoidal categories. Theory and Applications of Categories\u00a026(23), 582\u2013659 (2012)","journal-title":"Theory and Applications of Categories"},{"key":"7_CR12","unstructured":"Schreiber, U.: Quantization via linear homotopy types. arXiv preprint arXiv:1402.7041 (2014)"},{"key":"7_CR13","unstructured":"V\u00e1k\u00e1r, M.: Syntax and semantics of linear dependent types. arXiv preprint arXiv:1405.0033 (original preprint from April 2014)"},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"Krishnaswami, N.R., Pradic, P., Benton, N.: Integrating dependent and linear types (July 2014), https:\/\/www.mpi-sws.org\/~neelk\/dlnl-paper.pdf","DOI":"10.1145\/2676726.2676969"},{"key":"7_CR15","unstructured":"Barber, A.: Dual intuitionistic linear logic. Technical Report ECS-LFCS-96-347, University of Edinburgh, Edinburgh (1996)"},{"key":"7_CR16","doi-asserted-by":"crossref","unstructured":"Hofmann, M.: Syntax and semantics of dependent types. In: Extensional Constructs in Intensional Type Theory, pp. 13\u201354. Springer (1997)","DOI":"10.1007\/978-1-4471-0963-1_2"},{"issue":"2","key":"7_CR17","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1016\/0304-3975(93)90169-T","volume":"107","author":"B. Jacobs","year":"1993","unstructured":"Jacobs, B.: Comprehension categories and the semantics of type dependency. Theoretical Computer Science\u00a0107(2), 169\u2013207 (1993)","journal-title":"Theoretical Computer Science"},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"Pitts, A.M.: Categorical logic. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science. Algebraic and Logical Structures, vol.\u00a05, pp. 39\u2013128. Oxford University Press (2000)","DOI":"10.1093\/oso\/9780198537816.003.0005"},{"key":"7_CR19","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1090\/pspum\/017\/0257175","volume":"17","author":"F.W. Lawvere","year":"1970","unstructured":"Lawvere, F.W.: Equality in hyperdoctrines and comprehension schema as an adjoint functor. Applications of Categorical Algebra\u00a017, 1\u201314 (1970)","journal-title":"Applications of Categorical Algebra"},{"key":"7_CR20","unstructured":"Abramsky, S., Duncan, R.: A categorical quantum logic. Mathematical Structures in Computer Science\u00a016(3), 469\u2013489 (2006), Preprint available at http:\/\/arxiv.org\/abs\/quant-ph\/0512114"}],"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_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T19:57:37Z","timestamp":1747857457000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46678-0_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662466773","9783662466780"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46678-0_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}