{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:12:23Z","timestamp":1775873543826,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":49,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,9,6]],"date-time":"2022-09-06T00:00:00Z","timestamp":1662422400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,9,6]]},"DOI":"10.1145\/3546189.3549919","type":"proceedings-article","created":{"date-parts":[[2022,9,6]],"date-time":"2022-09-06T20:24:01Z","timestamp":1662495841000},"page":"13-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["How to safely use extensionality in Liquid Haskell"],"prefix":"10.1145","author":[{"given":"Niki","family":"Vazou","sequence":"first","affiliation":[{"name":"IMDEA Software Institute, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Greenberg","sequence":"additional","affiliation":[{"name":"Stevens Institute of Technology, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,9,6]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Thorsten Altenkirch and Conor McBride. 2006. Towards Observational Type Theory. http:\/\/www.strictlypositive.org\/ott.pdf Unpublished manuscript \t\t\t\t\t  Thorsten Altenkirch and Conor McBride. 2006. Towards Observational Type Theory. http:\/\/www.strictlypositive.org\/ott.pdf Unpublished manuscript"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.274.1"},{"key":"e_1_3_2_1_3_1","unstructured":"Carlo Angiuli Kuen-Bang Hou (Favonia) and Robert Harper. 2018. Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities. In Computer Science Logic. http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2018\/9673 \t\t\t\t\t  Carlo Angiuli Kuen-Bang Hou (Favonia) and Robert Harper. 2018. Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities. In Computer Science Logic. http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2018\/9673"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796815000209"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-29436-6_3"},{"key":"e_1_3_2_1_6_1","volume-title":"The SMT-LIB Standard: Version 2.0. Department of Computer Science","author":"Barrett Clark","unstructured":"Clark Barrett , Aaron Stump , and Cesare Tinelli . 2010. The SMT-LIB Standard: Version 2.0. Department of Computer Science , The University of Iowa . www.SMT-LIB.org Clark Barrett, Aaron Stump, and Cesare Tinelli. 2010. The SMT-LIB Standard: Version 2.0. Department of Computer Science, The University of Iowa. www.SMT-LIB.org"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796812000032"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018620"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/636517.636527"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.TYPES.2015.5"},{"key":"e_1_3_2_1_11_1","volume-title":"Smith","author":"Constable Robert L.","year":"1986","unstructured":"Robert L. Constable , Stuart F. Allen , Mark Bromley , Rance Cleaveland , J. F. Cremer , R. W. Harper , Douglas J. Howe , Todd B. Knoblock , N. P. Mendler , Prakash Panangaden , James T. Sasaki , and Scott F . Smith . 1986 . Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall . isbn:978-0-13-451832-9 http:\/\/dl.acm.org\/citation.cfm?id=10510 Robert L. Constable, Stuart F. Allen, Mark Bromley, Rance Cleaveland, J. F. Cremer, R. W. Harper, Douglas J. Howe, Todd B. Knoblock, N. P. Mendler, Prakash Panangaden, James T. Sasaki, and Scott F. Smith. 1986. Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall. isbn:978-0-13-451832-9 http:\/\/dl.acm.org\/citation.cfm?id=10510"},{"key":"e_1_3_2_1_12_1","volume-title":"Partial objects in constructive type theory","author":"Constable Robert L","unstructured":"Robert L Constable and Scott Fraser Smith . 1987. Partial objects in constructive type theory . Cornell University . https:\/\/dl.acm.org\/doi\/10.5555\/866226 Robert L Constable and Scott Fraser Smith. 1987. Partial objects in constructive type theory. Cornell University. https:\/\/dl.acm.org\/doi\/10.5555\/866226"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000011"},{"key":"e_1_3_2_1_14_1","unstructured":"Github FStarLang. 2018. Functional Equality Discussions in F*.  https:\/\/github.com\/FStarLang\/FStar\/blob\/cba5383bd0e84140a00422875de21a8a77bae116\/ulib\/FStar.FunctionalExtensionality.fsti#L133-L134 \t\t\t\t\t  Github FStarLang. 2018. Functional Equality Discussions in F*.  https:\/\/github.com\/FStarLang\/FStar\/blob\/cba5383bd0e84140a00422875de21a8a77bae116\/ulib\/FStar.FunctionalExtensionality.fsti#L133-L134"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034777"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796812000135"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411218"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1667048.1667051"},{"key":"e_1_3_2_1_19_1","volume-title":"Scheme and Functional Programming Workshop. http:\/\/www.cs.williams.edu\/~freund\/papers\/06-sfp.pdf","author":"Knowles Kenneth","year":"2006","unstructured":"Kenneth Knowles , Aaron Tomb , Jessica Gronski , Stephen N. Freund , and Cormac Flanagan . 2006 . Sage: Hybrid checking for flexible specifications . In Scheme and Functional Programming Workshop. http:\/\/www.cs.williams.edu\/~freund\/papers\/06-sfp.pdf Kenneth Knowles, Aaron Tomb, Jessica Gronski, Stephen N. Freund, and Cormac Flanagan. 2006. Sage: Hybrid checking for flexible specifications. In Scheme and Functional Programming Workshop. http:\/\/www.cs.williams.edu\/~freund\/papers\/06-sfp.pdf"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158133"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2402676.2402682"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428284"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341708"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1989.39155"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_17"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159812"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158698"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/3540543961_1"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/1-4020-8141-3_34"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.713327"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2994594"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434307"},{"key":"e_1_3_2_1_34_1","unstructured":"Matthieu Sozeau. 2008. Un environnement pour la programmation avec types d\u00e9pendants. Ph. D. Dissertation. Universit\u00e9 Paris 11. https:\/\/tel.archives-ouvertes.fr\/tel-00640052 \t\t\t\t\t  Matthieu Sozeau. 2008. Un environnement pour la programmation avec types d\u00e9pendants. Ph. D. Dissertation. Universit\u00e9 Paris 11. https:\/\/tel.archives-ouvertes.fr\/tel-00640052"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_23"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2019.31"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2491978"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_30"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3429979"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3242744.3242756"},{"key":"#cr-split#-e_1_3_2_1_42_1.1","doi-asserted-by":"crossref","unstructured":"Niki Vazou and Michael Greenberg. 2021. How to Safely Use Extensionality in Liquid Haskell (extended version). In CoRR. https:\/\/doi.org\/10.48550\/ARXIV.2103.02177 10.48550\/ARXIV.2103.02177","DOI":"10.1145\/3554301"},{"key":"#cr-split#-e_1_3_2_1_42_1.2","doi-asserted-by":"crossref","unstructured":"Niki Vazou and Michael Greenberg. 2021. How to Safely Use Extensionality in Liquid Haskell (extended version). In CoRR. https:\/\/doi.org\/10.48550\/ARXIV.2103.02177","DOI":"10.1145\/3554301"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158141"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75283"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009923"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028402"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/277650.277732"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371119"}],"event":{"name":"Haskell '22: 15th ACM SIGPLAN International Haskell Symposium","location":"Ljubljana Slovenia","acronym":"Haskell '22","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 15th ACM SIGPLAN International Haskell Symposium"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3546189.3549919","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3546189.3549919","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:00:23Z","timestamp":1750186823000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3546189.3549919"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,9,6]]},"references-count":49,"alternative-id":["10.1145\/3546189.3549919","10.1145\/3546189"],"URL":"https:\/\/doi.org\/10.1145\/3546189.3549919","relation":{},"subject":[],"published":{"date-parts":[[2022,9,6]]},"assertion":[{"value":"2022-09-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}