{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:26:42Z","timestamp":1767929202118,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":24,"publisher":"ACM","license":[{"start":{"date-parts":[[2007,10,2]],"date-time":"2007-10-02T00:00:00Z","timestamp":1191283200000},"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":[[2007,10,2]]},"DOI":"10.1145\/1292597.1292608","type":"proceedings-article","created":{"date-parts":[[2007,10,14]],"date-time":"2007-10-14T12:51:38Z","timestamp":1192366298000},"page":"57-68","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":69,"title":["Observational equality, now!"],"prefix":"10.1145","author":[{"given":"Thorsten","family":"Altenkirch","sequence":"first","affiliation":[{"name":"University of Nottingham, Nottingham, United Kingdom"}]},{"given":"Conor","family":"McBride","sequence":"additional","affiliation":[{"name":"University of Nottingham, Nottingham, United Kingdom"}]},{"given":"Wouter","family":"Swierstra","sequence":"additional","affiliation":[{"name":"University of Nottingham, Nottingham, United Kingdom"}]}],"member":"320","published-online":{"date-parts":[[2007,10,2]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.06.002"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.33"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/788021.788977"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/289423.289451"},{"key":"e_1_3_2_1_6_1","volume-title":"International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice","author":"Buisse Alexandre","year":"2007","unstructured":"Alexandre Buisse and Peter Dybjer . Formalizing categorical models of type theory in type theory . In International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice , 2007 . Alexandre Buisse and Peter Dybjer. Formalizing categorical models of type theory in type theory. In International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2007."},{"key":"e_1_3_2_1_7_1","volume-title":"Implementing Mathematics with the Nuprl Development System","author":"Constable Robert L.","year":"1986","unstructured":"Robert L. Constable , Stuart F. Allen , HM. Bromley , WR. Cleaveland , JF. Cremer , RW. Harper , Douglas J. Howe , TB. Knoblock , NP. Mendler , P. Panangaden , James T. Sasaki , and Scott F. Smith . Implementing Mathematics with the Nuprl Development System . Prentice-Hall , 1986 . Robert L. Constable, Stuart F. Allen, HM. Bromley, WR. Cleaveland, JF. Cremer, RW. Harper, Douglas J. Howe, TB. Knoblock, NP. Mendler, P. Panangaden, James T. Sasaki, and Scott F. Smith. Implementing Mathematics with the Nuprl Development System. Prentice-Hall, 1986."},{"key":"e_1_3_2_1_8_1","first-page":"71","volume-title":"Informal Proceedings Workshop on Types for Proofs and Programs","author":"Coquand Thierry","year":"1992","unstructured":"Thierry Coquand . Pattern matching with dependent types. In BNordstr\u00f6m, KPettersson, and GPlotkin, editors , Informal Proceedings Workshop on Types for Proofs and Programs , B\u00e5stad, Sweden, 8- -12 June 1992 , pages 71 -- 84 . Dept. of Computing Science, Chalmers Univ. of Technology and G\u00f6teborg Univ., 1992. Thierry Coquand. Pattern matching with dependent types. In BNordstr\u00f6m, KPettersson, and GPlotkin, editors, Informal Proceedings Workshop on Types for Proofs and Programs, B\u00e5stad, Sweden, 8--12 June 1992, pages 71--84. Dept. of Computing Science, Chalmers Univ. of Technology and G\u00f6teborg Univ., 1992."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/645894.671773"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/120477.120487"},{"key":"e_1_3_2_1_11_1","volume-title":"Epigram","author":"Conor","year":"2004","unstructured":"Conor McBride et al . Epigram , 2004 . http:\/\/www.e-pig.org. Conor McBride et al. Epigram, 2004. http:\/\/www.e-pig.org."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/11780274_27"},{"key":"e_1_3_2_1_13_1","first-page":"153","volume-title":"TYPES 95","author":"Hofmann Martin","year":"1995","unstructured":"Martin Hofmann . Conservativity of equality reflection over intensional type theory . In TYPES 95 , pages 153 -- 164 , 1995 . Martin Hofmann. Conservativity of equality reflection over intensional type theory. In TYPES 95, pages 153--164, 1995."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1994.316071"},{"key":"e_1_3_2_1_16_1","volume-title":"Constructive Category Theory","author":"Sa\u00efbi Huet","year":"1998","unstructured":"G Huet and A Sa\u00efbi . Constructive Category Theory . MIT Press , 1998 . GHuet and ASa\u00efbi. Constructive Category Theory. MIT Press, 1998."},{"key":"e_1_3_2_1_17_1","volume-title":"Computation and Reasoning: A Type Theory for Computer Science","author":"Luo Zhaohui","year":"1994","unstructured":"Zhaohui Luo . Computation and Reasoning: A Type Theory for Computer Science . Oxford University Press , 1994 . Zhaohui Luo. Computation and Reasoning: A Type Theory for Computer Science. Oxford University Press, 1994."},{"key":"e_1_3_2_1_19_1","volume-title":"Types for Proofs and Programs (Proceedings of the International Workshop, TYPES'00)","volume":"2277","author":"McBride Conor","year":"2002","unstructured":"Conor McBride . Elimination with a Motive. In Paul Callaghan, Zhaohui Luo, James McKinna, and Robert Pollack, editors , Types for Proofs and Programs (Proceedings of the International Workshop, TYPES'00) , volume 2277 . Springer-Verlag , 2002 . Conor McBride. Elimination with a Motive. In Paul Callaghan, Zhaohui Luo, James McKinna, and Robert Pollack, editors, Types for Proofs and Programs (Proceedings of the International Workshop, TYPES'00), volume 2277. Springer-Verlag, 2002."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796803004829"},{"key":"e_1_3_2_1_21_1","unstructured":"Ulf Norell. Agda 2. http:\/\/appserv.cs.chalmers.se\/users\/ulfn\/wiki\/agda.php.  Ulf Norell. Agda 2. http:\/\/appserv.cs.chalmers.se\/users\/ulfn\/wiki\/agda.php."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_18"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75285"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159811"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1088348.1088356"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190315.1190324"},{"key":"e_1_3_2_1_27_1","volume-title":"Proceedings of the Workshop on Programming Logic. Programming Methodology Group, University of Gothenburg and Chalmers University of Technology","author":"Turner David A.","year":"1989","unstructured":"David A. Turner . A new formulation of constructive type theory. In Peter Dybjer et al., editor , Proceedings of the Workshop on Programming Logic. Programming Methodology Group, University of Gothenburg and Chalmers University of Technology , 1989 . David A. Turner. A new formulation of constructive type theory. In Peter Dybjer et al., editor, Proceedings of the Workshop on Programming Logic. Programming Methodology Group, University of Gothenburg and Chalmers University of Technology, 1989."}],"event":{"name":"ICFP07: ACM SIGPLAN International Conference on Functional Programming","location":"Freiburg Germany","acronym":"ICFP07","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery"]},"container-title":["Proceedings of the 2007 workshop on Programming languages meets program verification"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1292597.1292608","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1292597.1292608","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T14:52:27Z","timestamp":1750258347000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1292597.1292608"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,10,2]]},"references-count":24,"alternative-id":["10.1145\/1292597.1292608","10.1145\/1292597"],"URL":"https:\/\/doi.org\/10.1145\/1292597.1292608","relation":{},"subject":[],"published":{"date-parts":[[2007,10,2]]},"assertion":[{"value":"2007-10-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}