{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:32:31Z","timestamp":1750221151277,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":31,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,7,9]],"date-time":"2018-07-09T00:00:00Z","timestamp":1531094400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Labex DigiCosme","award":["ANR11LABEX0045DIGICOSME"],"award-info":[{"award-number":["ANR11LABEX0045DIGICOSME"]}]},{"name":"Idex ParisSaclay","award":["ANR11IDEX000302"],"award-info":[{"award-number":["ANR11IDEX000302"]}]},{"name":"UK EPSRC","award":["EP\/K037633\/1"],"award-info":[{"award-number":["EP\/K037633\/1"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2018,7,9]]},"DOI":"10.1145\/3209108.3209206","type":"proceedings-article","created":{"date-parts":[[2018,6,27]],"date-time":"2018-06-27T12:14:43Z","timestamp":1530101683000},"page":"95-104","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Extensional and Intensional Semantic Universes"],"prefix":"10.1145","author":[{"given":"Valentin","family":"Blot","sequence":"first","affiliation":[{"name":"LRI, Universit\u00e9 Paris Sud, CNRS, Universit\u00e9 Paris-Saclay, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jim","family":"Laird","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Bath, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2018,7,9]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.2307\/2275407"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2004.10.002"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2930"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-47666-6_3"},{"key":"e_1_3_2_1_5_1","unstructured":"Thorsten Altenkirch Conor McBride and James McKinna. 2005. Why dependent types matter. (2005). http:\/\/www.e-pig.org\/downloads\/ydtm.pdf.  Thorsten Altenkirch Conor McBride and James McKinna. 2005. Why dependent types matter. (2005). http:\/\/www.e-pig.org\/downloads\/ydtm.pdf."},{"volume-title":"Cambridge Tracts in Theoretical Computer Science","author":"Amadio Roberto","key":"e_1_3_2_1_6_1","unstructured":"Roberto Amadio and Pierre-Louis Curien . 1998. Domains and Lambda-Calculi . Cambridge Tracts in Theoretical Computer Science , Vol. 46 . Cambridge University Press . Roberto Amadio and Pierre-Louis Curien. 1998. Domains and Lambda-Calculi. Cambridge Tracts in Theoretical Computer Science, Vol. 46. Cambridge University Press."},{"volume-title":"Handbook of Logic in Computer Science.","author":"Barendregt Henk","key":"e_1_3_2_1_7_1","unstructured":"Henk Barendregt . 1992. Lambda Calculi with Types . In Handbook of Logic in Computer Science. Vol. 2 . Oxford University Press , 117--309. Henk Barendregt. 1992. Lambda Calculi with Types. In Handbook of Logic in Computer Science. Vol. 2. Oxford University Press, 117--309."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1051\/ita\/197610R100471","article-title":"Bottom-Up Computation of Recursive Programs","volume":"10","author":"Berry G\u00e9rard","year":"1976","unstructured":"G\u00e9rard Berry . 1976 . Bottom-Up Computation of Recursive Programs . Informatique Th\u00e9orique et Applications 10 , 1 (1976), 47 -- 82 . G\u00e9rard Berry. 1976. Bottom-Up Computation of Recursive Programs. Informatique Th\u00e9orique et Applications 10, 1 (1976), 47--82.","journal-title":"Informatique Th\u00e9orique et Applications"},{"volume-title":"5th Colloquium on Automata, Languages and Programming","author":"Berry G\u00e9rard","key":"e_1_3_2_1_9_1","unstructured":"G\u00e9rard Berry . 1978. Stable Models of Typed lambda-Calculi . In 5th Colloquium on Automata, Languages and Programming . Springer , 72--89. G\u00e9rard Berry. 1978. Stable Models of Typed lambda-Calculi. In 5th Colloquium on Automata, Languages and Programming. Springer, 72--89."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(82)80002-9"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1047"},{"key":"e_1_3_2_1_12_1","volume-title":"Least and Greatest Fixpoints in Game Semantics. In 12th International Conference on Foundations Of Software Science And Computational Structures (Lecture Notes in Computer Science). Springer, 16--31","author":"Clairambault Pierre","year":"2009","unstructured":"Pierre Clairambault . 2009 . Least and Greatest Fixpoints in Game Semantics. In 12th International Conference on Foundations Of Software Science And Computational Structures (Lecture Notes in Computer Science). Springer, 16--31 . Pierre Clairambault. 2009. Least and Greatest Fixpoints in Game Semantics. In 12th International Conference on Foundations Of Software Science And Computational Structures (Lecture Notes in Computer Science). Springer, 16--31."},{"key":"e_1_3_2_1_13_1","volume-title":"The biequivalence of locally cartesian closed categories and Martin-L\u00f6f type theories. Mathematical Structures in Computer Science 24, 6","author":"Clairambault Pierre","year":"2014","unstructured":"Pierre Clairambault and Peter Dybjer . 2014. The biequivalence of locally cartesian closed categories and Martin-L\u00f6f type theories. Mathematical Structures in Computer Science 24, 6 ( 2014 ). Pierre Clairambault and Peter Dybjer. 2014. The biequivalence of locally cartesian closed categories and Martin-L\u00f6f type theories. Mathematical Structures in Computer Science 24, 6 (2014)."},{"key":"e_1_3_2_1_14_1","volume-title":"Observable Algorithms on Concrete Data Structures. In 7th Annual Symposium on Logic in Computer Science. IEEE Computer Society, 432--443","author":"Curien Pierre-Louis","year":"1992","unstructured":"Pierre-Louis Curien . 1992 . Observable Algorithms on Concrete Data Structures. In 7th Annual Symposium on Logic in Computer Science. IEEE Computer Society, 432--443 . Pierre-Louis Curien. 1992. Observable Algorithms on Concrete Data Structures. In 7th Annual Symposium on Logic in Computer Science. IEEE Computer Society, 432--443."},{"key":"e_1_3_2_1_15_1","volume-title":"Internal Type Theory. In International Workshop on Types for Proofs and Programs, Selected Papers. Springer, 120--134","author":"Dybjer Peter","year":"1995","unstructured":"Peter Dybjer . 1995 . Internal Type Theory. In International Workshop on Types for Proofs and Programs, Selected Papers. Springer, 120--134 . Peter Dybjer. 1995. Internal Type Theory. In International Workshop on Types for Proofs and Programs, Selected Papers. Springer, 120--134."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/11417170_16"},{"key":"e_1_3_2_1_17_1","volume-title":"Proceedings of a Congress held in Venice","author":"Hofmann Martin","year":"1998","unstructured":"Martin Hofmann and Thomas Streicher . 1998 . The Groupoid Interpretation of Type Theory. In Twenty-Five Years of Constructive Type Theory , Proceedings of a Congress held in Venice , October 1995 (Oxford Logic Guides). Oxford University Press, 83--111. Martin Hofmann and Thomas Streicher. 1998. The Groupoid Interpretation of Type Theory. In Twenty-Five Years of Constructive Type Theory, Proceedings of a Congress held in Venice, October 1995 (Oxford Logic Guides). Oxford University Press, 83--111."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2917"},{"key":"e_1_3_2_1_19_1","volume-title":"Games on Graphs and Sequentially Realizable Functionals. In 17th IEEE Symposium on Logic in Computer Science. IEEE Computer Society, 257--264","author":"Hyland Martin","year":"2002","unstructured":"Martin Hyland and Andrea Schalk . 2002 . Games on Graphs and Sequentially Realizable Functionals. In 17th IEEE Symposium on Logic in Computer Science. IEEE Computer Society, 257--264 . Martin Hyland and Andrea Schalk. 2002. Games on Graphs and Sequentially Realizable Functionals. In 17th IEEE Symposium on Logic in Computer Science. IEEE Computer Society, 257--264."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90090-G"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90090-G"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2508028.2505986"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00194-8"},{"volume-title":"Studies in Logic and the Foundations of Mathematics.","author":"Martin-L\u00f6f Per","key":"e_1_3_2_1_24_1","unstructured":"Per Martin-L\u00f6f . 1982. Constructive mathematics and computer programming . In Studies in Logic and the Foundations of Mathematics. Vol. 104 . Elsevier , 153--175. Per Martin-L\u00f6f. 1982. Constructive mathematics and computer programming. In Studies in Logic and the Foundations of Mathematics. Vol. 104. Elsevier, 153--175."},{"key":"e_1_3_2_1_25_1","unstructured":"Per Martin-L\u00f6f. 1984. Intuitionistic Type Theory. Bibliopolis.  Per Martin-L\u00f6f. 1984. Intuitionistic Type Theory. Bibliopolis."},{"volume-title":"Games and full abstraction for a functional metalanguage with recursive types","author":"McCusker Guy","key":"e_1_3_2_1_26_1","unstructured":"Guy McCusker . 1998. Games and full abstraction for a functional metalanguage with recursive types . Springer . Guy McCusker. 1998. Games and full abstraction for a functional metalanguage with recursive types. Springer."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1993.1048"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(90)90044-3"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(90)90044-3"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0052"},{"key":"e_1_3_2_1_31_1","volume-title":"Probabilistic Event Structures and Domains. In 15th International Conference on Concurrency Theory. Springer, 481--496","author":"Varacca Daniele","year":"2004","unstructured":"Daniele Varacca , Hagen V\u00f6lzer , and Glynn Winskel . 2004 . Probabilistic Event Structures and Domains. In 15th International Conference on Concurrency Theory. Springer, 481--496 . Daniele Varacca, Hagen V\u00f6lzer, and Glynn Winskel. 2004. Probabilistic Event Structures and Domains. In 15th International Conference on Concurrency Theory. Springer, 481--496."}],"event":{"name":"LICS '18: 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science","sponsor":["SIGLOG ACM Special Interest Group on Logic and Computation","EACSL European Association for Computer Science Logic","IEEE-CS\\DATC IEEE Computer Society"],"location":"Oxford United Kingdom","acronym":"LICS '18"},"container-title":["Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3209108.3209206","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3209108.3209206","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T01:08:24Z","timestamp":1750208904000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3209108.3209206"}},"subtitle":["A Denotational Model of Dependent Types"],"short-title":[],"issued":{"date-parts":[[2018,7,9]]},"references-count":31,"alternative-id":["10.1145\/3209108.3209206","10.1145\/3209108"],"URL":"https:\/\/doi.org\/10.1145\/3209108.3209206","relation":{},"subject":[],"published":{"date-parts":[[2018,7,9]]},"assertion":[{"value":"2018-07-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}