{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T09:43:08Z","timestamp":1770284588330,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":15,"publisher":"ACM","license":[{"start":{"date-parts":[[2016,7,5]],"date-time":"2016-07-05T00:00:00Z","timestamp":1467676800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"ERC Starting Grant","award":["637339"],"award-info":[{"award-number":["637339"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2016,7,5]]},"DOI":"10.1145\/2933575.2935320","type":"proceedings-article","created":{"date-parts":[[2016,10,14]],"date-time":"2016-10-14T13:34:47Z","timestamp":1476452087000},"page":"367-376","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":14,"title":["The Definitional Side of the Forcing"],"prefix":"10.1145","author":[{"given":"Guilhem","family":"Jaber","sequence":"first","affiliation":[{"name":"IRIF - Universit\u00e9 Paris Diderot, \u03c0r2, Inria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gabriel","family":"Lewertowski","sequence":"additional","affiliation":[{"name":"IRIF - Universit\u00e9 Paris Diderot, \u03c0r2, Inria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pierre-Marie","family":"P\u00e9drot","sequence":"additional","affiliation":[{"name":"Inria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matthieu","family":"Sozeau","sequence":"additional","affiliation":[{"name":"IRIF - Universit\u00e9 Paris Diderot, \u03c0r2, Inria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nicolas","family":"Tabareau","sequence":"additional","affiliation":[{"name":"Inria"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2016,7,5]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837638"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/1987171.1987181"},{"key":"e_1_3_2_1_4_1","volume-title":"Cubical Type Theory: a constructive interpretation of the univalence axiom","author":"Cohen C.","year":"2015","unstructured":"C. Cohen , T. Coquand , S. Huber , and A. M\u00f6rtberg . Cubical Type Theory: a constructive interpretation of the univalence axiom , 2015 . Preprint . C. Cohen, T. Coquand, S. Huber, and A. M\u00f6rtberg. Cubical Type Theory: a constructive interpretation of the univalence axiom, 2015. Preprint."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.47"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.49"},{"key":"e_1_3_2_1_7_1","volume-title":"The simplicial model of univalent foundations. arXiv preprint arXiv:1211.2851","author":"Kapulkin C.","year":"2012","unstructured":"C. Kapulkin , P. L. Lumsdaine , and V. Voevodsky . The simplicial model of univalent foundations. arXiv preprint arXiv:1211.2851 , 2012 . C. Kapulkin, P. L. Lumsdaine, and V. Voevodsky. The simplicial model of univalent foundations. arXiv preprint arXiv:1211.2851, 2012."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(94)90047-7"},{"key":"e_1_3_2_1_9_1","first-page":"197","article-title":"Realizability in classical logic","volume":"27","author":"Krivine J.-L.","year":"2009","unstructured":"J.-L. Krivine . Realizability in classical logic . Panoramas et synth\u00e8ses , 27 : 197 -- 229 , 2009 . J.-L. Krivine. Realizability in classical logic. Panoramas et synth\u00e8ses, 27:197--229, 2009.","journal-title":"Panoramas et synth\u00e8ses"},{"key":"e_1_3_2_1_10_1","unstructured":"P. B. Levy. Call-by-push-value. PhD thesis Queen Mary University of London 2001.  P. B. Levy. Call-by-push-value. PhD thesis Queen Mary University of London 2001."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/77350.77390"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2011.47"},{"key":"e_1_3_2_1_13_1","first-page":"317","volume-title":"13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015","volume":"38","author":"Scherer G.","year":"2015","unstructured":"G. Scherer . Multi-focusing on extensional rewriting with sums. In T. Altenkirch, editor , 13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015 , July 1-3, 2015 , Warsaw, Poland , volume 38 of LIPIcs, pages 317 -- 331 . Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. ISBN 978-3-939897-87-3. G. Scherer. Multi-focusing on extensional rewriting with sums. In T. Altenkirch, editor, 13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015, July 1-3, 2015, Warsaw, Poland, volume 38 of LIPIcs, pages 317--331. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. ISBN 978-3-939897-87-3."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1007\/BFb0073963","volume-title":"Toposes, algebraic geometry and logic","author":"Tierney M.","year":"1972","unstructured":"M. Tierney . Sheaf theory and the continuum hypothesis . In Toposes, algebraic geometry and logic , pages 13 -- 42 . Springer , 1972 . M. Tierney. Sheaf theory and the continuum hypothesis. In Toposes, algebraic geometry and logic, pages 13--42. Springer, 1972."},{"key":"e_1_3_2_1_15_1","unstructured":"Univalent Foundations Project. Homotopy Type Theory: Univalent Foundations for Mathematics. http:\/\/homotopytypetheory.org\/book 2013.  Univalent Foundations Project. Homotopy Type Theory: Univalent Foundations for Mathematics. http:\/\/homotopytypetheory.org\/book 2013."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"crossref","first-page":"530","DOI":"10.1007\/BFb0014566","volume-title":"Theoretical aspects of computer software","author":"Werner B.","year":"1997","unstructured":"B. Werner . Sets in types, types in sets . In Theoretical aspects of computer software , pages 530 -- 546 . Springer , 1997 . B. Werner. Sets in types, types in sets. In Theoretical aspects of computer software, pages 530--546. Springer, 1997."}],"event":{"name":"LICS '16: 31st Annual ACM\/IEEE Symposium on Logic in Computer Science","location":"New York NY USA","acronym":"LICS '16","sponsor":["SIGLOG ACM Special Interest Group on Logic and Computation","EACSL European Association for Computer Science Logic","IEEE-CS\\DATC IEEE Computer Society"]},"container-title":["Proceedings of the 31st Annual ACM\/IEEE Symposium on Logic in Computer Science"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2933575.2935320","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2933575.2935320","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:54:54Z","timestamp":1750222494000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2933575.2935320"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,7,5]]},"references-count":15,"alternative-id":["10.1145\/2933575.2935320","10.1145\/2933575"],"URL":"https:\/\/doi.org\/10.1145\/2933575.2935320","relation":{},"subject":[],"published":{"date-parts":[[2016,7,5]]},"assertion":[{"value":"2016-07-05","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}