{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,11]],"date-time":"2026-05-11T17:25:32Z","timestamp":1778520332036,"version":"3.51.4"},"publisher-location":"New York, NY, USA","reference-count":29,"publisher":"ACM","license":[{"start":{"date-parts":[[2006,1,11]],"date-time":"2006-01-11T00:00:00Z","timestamp":1136937600000},"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":[[2006,1,11]]},"DOI":"10.1145\/1111037.1111056","type":"proceedings-article","created":{"date-parts":[[2006,2,6]],"date-time":"2006-02-06T10:52:40Z","timestamp":1139223160000},"page":"206-217","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":35,"title":["Fast and loose reasoning is morally correct"],"prefix":"10.1145","author":[{"given":"Nils Anders","family":"Danielsson","sequence":"first","affiliation":[{"name":"Chalmers University of Technology"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John","family":"Hughes","sequence":"additional","affiliation":[{"name":"Chalmers University of Technology"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Patrik","family":"Jansson","sequence":"additional","affiliation":[{"name":"Chalmers University of Technology"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jeremy","family":"Gibbons","sequence":"additional","affiliation":[{"name":"Oxford University Computing Laboratory"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2006,1,11]]},"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_2_1","first-page":"1","volume-title":"Proceedings of Symposia in Mathematical Logic, Oulu, 1974","author":"Aczel Peter","year":"1975","unstructured":"Peter Aczel . The strength of Martin-L\u00f6f's intuitionistic type theory with one universe . In Proceedings of Symposia in Mathematical Logic, Oulu, 1974 , and Helsinki , 1975 , pages 1 -- 32 , University of Helsinki, Department of Philosophy, 1977. Peter Aczel. The strength of Martin-L\u00f6f's intuitionistic type theory with one universe. In Proceedings of Symposia in Mathematical Logic, Oulu, 1974, and Helsinki, 1975, pages 1--32, University of Helsinki, Department of Philosophy, 1977."},{"key":"e_1_3_2_1_3_1","series-title":"LNCS","first-page":"268","volume-title":"VDM '91","author":"Bednarczyk Marek A.","year":"1991","unstructured":"Marek A. Bednarczyk and Andrzej M. Borzyszkowski . Cpo's do not form a cpo and yet recursion works . In VDM '91 , volume 551 of LNCS , pages 268 -- 278 . Springer-Verlag , 1991 . Marek A. Bednarczyk and Andrzej M. Borzyszkowski. Cpo's do not form a cpo and yet recursion works. In VDM '91, volume 551 of LNCS, pages 268--278. Springer-Verlag, 1991."},{"key":"e_1_3_2_1_4_1","first-page":"287","volume-title":"Constructing Programs from Specifications","author":"Backhouse R.C.","year":"1991","unstructured":"R.C. Backhouse , P.J. de Bruin , P. Hoogendijk , G. Malcolm , T.S. Voermans , and J.C.S. P. van~der Woude. Relational catamorphisms . In Constructing Programs from Specifications , pages 287 -- 318 . North-Holland , 1991 . R.C. Backhouse, P.J. de Bruin, P. Hoogendijk, G. Malcolm, T.S. Voermans, and J.C.S.P. van~der Woude. Relational catamorphisms. In Constructing Programs from Specifications, pages 287--318. North-Holland, 1991."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/248932"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/0003-4843(82)90003-1"},{"key":"e_1_3_2_1_7_1","series-title":"LNCS","volume-title":"Towards a Metalanguage for Applied Denotational Semantics","author":"Blikle Andrzej","year":"1987","unstructured":"Andrzej Blikle . MetaSoft Primer , Towards a Metalanguage for Applied Denotational Semantics , volume 288 of LNCS . Springer-Verlag , 1987 . Andrzej Blikle. MetaSoft Primer, Towards a Metalanguage for Applied Denotational Semantics, volume 288 of LNCS. Springer-Verlag, 1987."},{"key":"e_1_3_2_1_8_1","first-page":"345","volume-title":"Information Processing 83","author":"Blikle Andrzej","year":"1983","unstructured":"Andrzej Blikle and Andrzej Tarlecki . Naive denotational semantics . In Information Processing 83 , pages 345 -- 355 . North-Holland , 1983 . Andrzej Blikle and Andrzej Tarlecki. Naive denotational semantics. In Information Processing 83, pages 345--355. North-Holland, 1983."},{"key":"e_1_3_2_1_9_1","volume-title":"Personal web page,","author":"Danielsson Nils Anders","year":"2005","unstructured":"Nils Anders Danielsson . Personal web page, available at http:\/\/www.cs.chalmers.se\/~nad\/, 2005 . Nils Anders Danielsson. Personal web page, available at http:\/\/www.cs.chalmers.se\/~nad\/, 2005."},{"key":"e_1_3_2_1_10_1","volume-title":"A Discipline of Programming","author":"Dijkstra Edsger W.","year":"1976","unstructured":"Edsger W. Dijkstra . A Discipline of Programming . Prentice Hall , 1976 . Edsger W. Dijkstra. A Discipline of Programming. Prentice Hall, 1976."},{"key":"e_1_3_2_1_11_1","first-page":"85","volume-title":"MPC 2004","volume":"3125","author":"Danielsson Nils Anders","year":"2004","unstructured":"Nils Anders Danielsson and Patrik Jansson . Chasing bottoms, a case study in program verification in the presence of partial and infinite values . In MPC 2004 , volume 3125 of LNCS, pages 85 -- 109 . Springer-Verlag , 2004 . Nils Anders Danielsson and Patrik Jansson. Chasing bottoms, a case study in program verification in the presence of partial and infinite values. In MPC 2004, volume 3125 of LNCS, pages 85--109. Springer-Verlag, 2004."},{"key":"e_1_3_2_1_12_1","series-title":"LNCS","first-page":"334","volume-title":"FPCA'85","author":"Dybjer Peter","year":"1985","unstructured":"Peter Dybjer . Program verification in a logical theory of constructions . In FPCA'85 , volume 201 of LNCS , pages 334 -- 349 . Springer-Verlag , 1985 . Appears in revised form as Programming Methodology Group Report 26, University of G\u00f6teborg and Chalmers University of Technology, 1986. Peter Dybjer. Program verification in a logical theory of constructions. In FPCA'85, volume 201 of LNCS, pages 334--349. Springer-Verlag, 1985. Appears in revised form as Programming Methodology Group Report 26, University of G\u00f6teborg and Chalmers University of Technology, 1986."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(96)00145-4"},{"key":"e_1_3_2_1_15_1","series-title":"Lecture Notes in Mathematics","first-page":"22","volume-title":"Logic Colloquium: Symposium on Logic held at Boston","author":"Friedman Harvey","year":"1972","unstructured":"Harvey Friedman . Equality between functionals . In Logic Colloquium: Symposium on Logic held at Boston , 1972 -73, number 453 in Lecture Notes in Mathematics , pages 22 -- 37 . Springer , 1975. Harvey Friedman. Equality between functionals. In Logic Colloquium: Symposium on Logic held at Boston, 1972-73, number 453 in Lecture Notes in Mathematics, pages 22--37. Springer, 1975."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90073-9"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(00)00220-9"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(90)90165-E"},{"key":"e_1_3_2_1_19_1","first-page":"247","volume-title":"Programming Concepts and Methods","author":"Jeuring J.","year":"1990","unstructured":"J. Jeuring . Algorithms from theorems . In Programming Concepts and Methods , pages 247 -- 266 . North-Holland , 1990 . J. Jeuring. Algorithms from theorems. In Programming Concepts and Methods, pages 247--266. North-Holland, 1990."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964010"},{"key":"e_1_3_2_1_21_1","series-title":"LNCS","first-page":"124","volume-title":"FPCA'91","author":"Meijer E.","year":"1991","unstructured":"E. Meijer , M. Fokkinga , and R. Paterson . Functional programming with bananas, lenses, envelopes and barbed wire . In FPCA'91 , volume 523 of LNCS , pages 124 -- 144 . Springer-Verlag , 1991 . E. Meijer, M. Fokkinga, and R. Paterson. Functional programming with bananas, lenses, envelopes and barbed wire. In FPCA'91, volume 523 of LNCS, pages 124--144. Springer-Verlag, 1991."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/549659"},{"key":"e_1_3_2_1_23_1","volume-title":"The Revised Report","author":"Jones Simon Peyton","year":"2003","unstructured":"Simon Peyton Jones , editor. Haskell 98 Language and Libraries , The Revised Report . Cambridge University Press , 2003 . Simon Peyton Jones, editor. Haskell 98 Language and Libraries, The Revised Report. Cambridge University Press, 2003."},{"key":"e_1_3_2_1_24_1","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1007\/3-540-47797-7_2","volume-title":"Algebraic and Coalgebraic Methods in the Mathematics of Program Construction","author":"Priestley Hilary A.","year":"2002","unstructured":"Hilary A. Priestley . Ordered sets and complete lattices, a primer for computer science . In Algebraic and Coalgebraic Methods in the Mathematics of Program Construction , volume 2297 of LNCS , chapter~2, pages 21 -- 78 . Springer-Verlag , 2002 . Hilary A. Priestley. Ordered sets and complete lattices, a primer for computer science. In Algebraic and Coalgebraic Methods in the Mathematics of Program Construction, volume 2297 of LNCS, chapter~2, pages 21--78. Springer-Verlag, 2002."},{"key":"e_1_3_2_1_25_1","first-page":"513","volume-title":"Information Processing 83","author":"Reynolds John C.","year":"1983","unstructured":"John C. Reynolds . Types , abstraction and parametric polymorphism . In Information Processing 83 , pages 513 -- 523 . Elsevier , 1983 . John C. Reynolds. Types, abstraction and parametric polymorphism. In Information Processing 83, pages 513--523. Elsevier, 1983."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-13346-1_7"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1137\/0205037"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.2307\/2274128"},{"key":"e_1_3_2_1_29_1","series-title":"LNCS","first-page":"1","volume-title":"FPLE'95","author":"Turner David","year":"1996","unstructured":"David Turner . Elementary strong functional programming . In FPLE'95 , volume 1022 of LNCS , pages 1 -- 13 . Springer-Verlag , 1996 . David Turner. Elementary strong functional programming. In FPLE'95, volume 1022 of LNCS, pages 1--13. Springer-Verlag, 1996."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/99370.99404"}],"event":{"name":"POPL06: The 33rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages 2006","location":"Charleston South Carolina USA","acronym":"POPL06","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1111037.1111056","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1111037.1111056","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T17:38:28Z","timestamp":1750268308000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1111037.1111056"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,1,11]]},"references-count":29,"alternative-id":["10.1145\/1111037.1111056","10.1145\/1111037"],"URL":"https:\/\/doi.org\/10.1145\/1111037.1111056","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1111320.1111056","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2006,1,11]]},"assertion":[{"value":"2006-01-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}