{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:56:23Z","timestamp":1776333383889,"version":"3.51.2"},"reference-count":11,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2006,10,1]],"date-time":"2006-10-01T00:00:00Z","timestamp":1159660800000},"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":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2006,10]]},"abstract":"<jats:p>\n            A\n            <jats:italic>quotient construction<\/jats:italic>\n            defines an abstract type from a concrete type, using an equivalence relation to identify elements of the concrete type that are to be regarded as indistinguishable. The elements of a quotient type are\n            <jats:italic>equivalence classes<\/jats:italic>\n            : sets of equivalent concrete values. Simple techniques are presented for defining and reasoning about quotient constructions, based on a general lemma library concerning functions that operate on equivalence classes. The techniques are applied to a definition of the integers from the natural numbers, and then to the definition of a recursive datatype satisfying equational constraints.\n          <\/jats:p>","DOI":"10.1145\/1183278.1183280","type":"journal-article","created":{"date-parts":[[2007,1,16]],"date-time":"2007-01-16T19:38:29Z","timestamp":1168976309000},"page":"658-675","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":20,"title":["Defining functions on equivalence classes"],"prefix":"10.1145","volume":"7","author":[{"given":"Lawrence C.","family":"Paulson","sequence":"first","affiliation":[{"name":"University of Cambridge, Cambridge, England"}]}],"member":"320","published-online":{"date-parts":[[2006,10]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"Crow J. Owre S. Rushby J. Shankar N. and Srivas M. 1995. A tutorial introduction to PVS. Tech. Rep. Computer Science Laboratory SRI International.  Crow J. Owre S. Rushby J. Shankar N. and Srivas M. 1995. A tutorial introduction to PVS. Tech. Rep. Computer Science Laboratory SRI International."},{"key":"e_1_2_1_2_1","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","article-title":"Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser","volume":"34","author":"de Bruijn N. G.","year":"1972","unstructured":"de Bruijn , N. G. 1972 . Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser Theorem. Ind. Math. 34 , 381 -- 392 . de Bruijn, N. G. 1972. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser Theorem. Ind. Math. 34, 381--392.","journal-title":"Theorem. Ind. Math."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.2002.0552"},{"key":"e_1_2_1_4_1","volume-title":"HOL: A Theorem Proving Environment for Higher Order Logic","author":"Gordon M. J. C.","year":"1993","unstructured":"Gordon , M. J. C. and Melham , T. F . 1993 . Introduction to HOL: A Theorem Proving Environment for Higher Order Logic . Cambridge University Press , Cambridge, MA . Gordon, M. J. C. and Melham, T. F. 1993. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge, MA."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01384233"},{"key":"e_1_2_1_6_1","volume-title":"TPHOLs 2001: Supplemental Proceedings","author":"Homeier P. V.","unstructured":"Homeier , P. V. 2001. Quotient types . In TPHOLs 2001: Supplemental Proceedings , R. J. Boulton and P. B. Jackson, Eds. Number EDI-INF-RR-0046 in Informatics Report Series. Division of Informatics, University of Edinburgh , 191--206. Online at http:\/\/www.informatics.ed.ac.uk\/publications\/report\/0046.html. Homeier, P. V. 2001. Quotient types. In TPHOLs 2001: Supplemental Proceedings, R. J. Boulton and P. B. Jackson, Eds. Number EDI-INF-RR-0046 in Informatics Report Series. Division of Informatics, University of Edinburgh, 191--206. Online at http:\/\/www.informatics.ed.ac.uk\/publications\/report\/0046.html."},{"key":"e_1_2_1_7_1","unstructured":"Kaufmann M. and Moore J. S. 2002. ACL2 Version 2.7. University of Texas at Austin Austin TX. (On the Internet at http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/v2-7\/.)  Kaufmann M. and Moore J. S. 2002. ACL2 Version 2.7. University of Texas at Austin Austin TX. (On the Internet at http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/v2-7\/.)"},{"key":"e_1_2_1_8_1","unstructured":"Kolman B. Busby R. C. and Ross S. C. 2000. Discrete Mathematical Structures 4th ed. Prentice-Hall Englewood Cliffs NJ.   Kolman B. Busby R. C. and Ross S. C. 2000. Discrete Mathematical Structures 4th ed. Prentice-Hall Englewood Cliffs NJ."},{"key":"e_1_2_1_9_1","doi-asserted-by":"crossref","unstructured":"Nipkow T. Paulson L. C. and Wenzel M. 2002. Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science tutorial 2283. Springer-Verlag New York.   Nipkow T. Paulson L. C. and Wenzel M. 2002. Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science tutorial 2283. Springer-Verlag New York.","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_2_1_10_1","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0028401","volume-title":"Theorem Proving in Higher Order Logics: TPHOLs '97","volume":"1275","author":"Slotosch O.","year":"1997","unstructured":"Slotosch , O. 1997 . Higher order quotients and their implementation in Isabelle HOL . In Theorem Proving in Higher Order Logics: TPHOLs '97 , E. L. Gunter and A. Felty, Eds. Lecture Notes in Computer Science , vol. 1275 . Springer-Verlag, New York, 291--306. Slotosch, O. 1997. Higher order quotients and their implementation in Isabelle HOL. In Theorem Proving in Higher Order Logics: TPHOLs '97, E. L. Gunter and A. Felty, Eds. Lecture Notes in Computer Science, vol. 1275. Springer-Verlag, New York, 291--306."},{"key":"e_1_2_1_11_1","volume-title":"CMCS 2004, 7th Workshop on Coalgebraic Methods in Computer Science, J. Ad\u00e1mek, Ed. Electronic Notes in Theoretical Computer Science. 361--378","author":"Tews H.","year":"2004","unstructured":"Tews , H. 2004 . Predicate and relation lifting for parametric algebraic specifications . In CMCS 2004, 7th Workshop on Coalgebraic Methods in Computer Science, J. Ad\u00e1mek, Ed. Electronic Notes in Theoretical Computer Science. 361--378 . Tews, H. 2004. Predicate and relation lifting for parametric algebraic specifications. In CMCS 2004, 7th Workshop on Coalgebraic Methods in Computer Science, J. Ad\u00e1mek, Ed. Electronic Notes in Theoretical Computer Science. 361--378."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1183278.1183280","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1183278.1183280","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T15:06:37Z","timestamp":1750259197000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1183278.1183280"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,10]]},"references-count":11,"aliases":["10.1145\/1166109.1166111"],"journal-issue":{"issue":"4","published-print":{"date-parts":[[2006,10]]}},"alternative-id":["10.1145\/1183278.1183280"],"URL":"https:\/\/doi.org\/10.1145\/1183278.1183280","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,10]]},"assertion":[{"value":"2006-10-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}