{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,5]],"date-time":"2026-05-05T09:54:20Z","timestamp":1777974860973,"version":"3.51.4"},"reference-count":52,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2009,3,4]],"date-time":"2009-03-04T00:00:00Z","timestamp":1236124800000},"content-version":"unspecified","delay-in-days":5298,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[1994,9]]},"abstract":"<jats:p>This paper surveys several different variants of order sorted algebra (abbreviated<jats:italic>OSA<\/jats:italic>), comparing some of the main approaches (overloaded OSA, universe OSA, unified algebra, term declaration algebra,<jats:italic>etc<\/jats:italic>.), emphasising motivation and intuitions, and pointing out features that distinguish the original \u2018overloaded\u2019 OSA approach from some later developments. These features include sort constraints and retracts; the latter is particularly useful for handling multiple data representations (including automatic coercions among them). Many examples are given, for most of which, runs are shown on the OBJ3 system.<\/jats:p><jats:p>This paper also significantly generalises overloaded OSA by dropping the regularity and monotonicity assumptions, and by adding signatures of non-monotonicities, which support simple semantics for some aspects of object oriented programming. A number of new results for this generalisation are proved, including initiality, variety, and quasi-variety theorems. Axiomatisability results \u00e0<jats:italic>la<\/jats:italic>Birkhoff are also proved for unified algebras.<\/jats:p>","DOI":"10.1017\/s0960129500000517","type":"journal-article","created":{"date-parts":[[2009,3,4]],"date-time":"2009-03-04T09:00:39Z","timestamp":1236157239000},"page":"363-392","source":"Crossref","is-referenced-by-count":54,"title":["An Oxford survey of order sorted algebra"],"prefix":"10.1017","volume":"4","author":[{"given":"Joseph","family":"Goguen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"R\u0103zvan","family":"Diaconescu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2009,3,4]]},"reference":[{"key":"S0960129500000517_ref050","first-page":"18","article-title":"Many-Sorted Inferences in Automated Theorem Proving. In: Sorts and Types in Artificial Intelligence","volume":"418","author":"Walther","year":"1990","journal-title":"Springer-Verlag Lecture Notes in Artificial Intelligence"},{"key":"S0960129500000517_ref049","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(85)90029-3"},{"key":"S0960129500000517_ref048","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90322-7"},{"key":"S0960129500000517_ref047","unstructured":"Strachey C. (1967) Fundamental Concepts in Programming Languages, Lecture Notes from International Summer School in Computer Programming, Copenhagen."},{"key":"S0960129500000517_ref045","unstructured":"Smolka G. (1986) Order-Sorted Horn Logic: Semantics and Deduction, Technical Report SEKI SR-86\u201317 Report, Fachbereich Informatik, Universit\u00e4t Kaiserslautern."},{"key":"S0960129500000517_ref052","unstructured":"Yan H. (1994) Theory and Implementation of Sort Constraints for Order Sorted Algebra, D. Phil. thesis, Programming Research Group, Oxford University."},{"key":"S0960129500000517_ref017","first-page":"119","volume-title":"A Classical Mind: Essays in Honour of C. A. R. Hoare","author":"Goguen","year":"1994"},{"key":"S0960129500000517_ref039","first-page":"329","volume-title":"Proceedings 16th Annual ACM Symposium on Principles of Programming Languages","author":"Mosses","year":"1989"},{"key":"S0960129500000517_ref022","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0014969"},{"key":"S0960129500000517_ref020","first-page":"295","volume-title":"Logic Programming: Functions, Relations and Equations","author":"Goguen","year":"1986"},{"key":"S0960129500000517_ref044","article-title":"Computational Aspects of an Order-Sorted Logic with Term Declarations","volume":"395","author":"Schmidt-Schauss","year":"1989","journal-title":"Springer-Verlag Lecture Notes in Artificial Intelligence"},{"key":"S0960129500000517_ref012","doi-asserted-by":"crossref","first-page":"357","DOI":"10.1093\/oso\/9780198537601.003.0014","volume-title":"Topology and Category Theory in Computer Science","author":"Goguen","year":"1991"},{"key":"S0960129500000517_ref042","volume-title":"Proceedings, Third Hungarian Computer Science Conference","author":"Reichel","year":"1981"},{"key":"S0960129500000517_ref016","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0015747"},{"key":"S0960129500000517_ref033","doi-asserted-by":"publisher","DOI":"10.1002\/mana.19630270108"},{"key":"S0960129500000517_ref043","first-page":"165","article-title":"Specifications in an Arbitrary Institution","volume":"76","author":"Sannella","year":"1988","journal-title":"Information and Control"},{"key":"S0960129500000517_ref008","first-page":"83","volume-title":"Logical Environments, Proceedings of a Workshop held in Edinburgh, Scotland, May 1991","author":"Diaconescu","year":"1993"},{"key":"S0960129500000517_ref028","doi-asserted-by":"publisher","DOI":"10.1145\/321992.321997"},{"key":"S0960129500000517_ref038","first-page":"304","volume-title":"Proceedings, Fourth Annual Conference on Logic in Computer Science","author":"Mosses","year":"1989"},{"key":"S0960129500000517_ref018","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0012775"},{"key":"S0960129500000517_ref051","volume-title":"A Treatise on Universal Algebra, with Applications, I","author":"Whitehead","year":"1898"},{"key":"S0960129500000517_ref030","first-page":"1","volume-title":"Object Oriented Databases: Analysis, Design and Construction","author":"Goguen","year":"1991"},{"key":"S0960129500000517_ref015","volume-title":"Proceedings, Tenth Workshop on Abstract Data Types","author":"Goguen","year":"1993"},{"key":"S0960129500000517_ref046","volume-title":"Resolution of Equations in Algebraic Structures, Volume 2: Rewriting Techniques","author":"Smolka","year":"1989"},{"key":"S0960129500000517_ref026","doi-asserted-by":"publisher","DOI":"10.1098\/rsta.1992.0026"},{"key":"S0960129500000517_ref023","first-page":"18","volume-title":"Proceedings, Second Symposium on Logic in Computer Science, Ithaca NY","author":"Goguen","year":"1987"},{"key":"S0960129500000517_ref002","first-page":"13","volume-title":"Colloquia Mathematics Societas J\u00e1nos Bolyai","author":"Andr\u00e9ka","year":"1981"},{"key":"S0960129500000517_ref004","first-page":"1","article-title":"Structures Alg\u00e9briques dans les Cat\u00e9gories","volume":"10","author":"Benabou","year":"1968","journal-title":"Cahiers de Topologie et G\u00e9ometrie Diff\u00e9rentiel"},{"key":"S0960129500000517_ref001","volume-title":"Term Declaration Logic and Generalised Composita","author":"Aczel","year":"1990"},{"key":"S0960129500000517_ref003","unstructured":"Antimirov V. and Degtyarev A. (1992) Consistency of Equational Enrichments. Proceedings, CRTS\u201992, St. Petersberg. Springer-Verlag Lecture Notes in Computer Science."},{"key":"S0960129500000517_ref005","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004100013463"},{"key":"S0960129500000517_ref032","unstructured":"Harper R. , MacQueen D. and Milner R. (1986) Standard ML, Technical Report ECS-LFCS-86\u20132, Department of Computer Science, University of Edinburgh."},{"key":"S0960129500000517_ref006","unstructured":"Burstall R. and Diaconescu R. (1992) Hiding and Behaviour: an Institutional Approach, Technical report ECS-LFCS-8892\u2013253, Laboratory for Foundations of Computer Science, University of Edinburgh. (Also in Roscoe, A. W. (ed.) (1994) A Classical Mind: Essays in Honour of C. A. R. Hoare Prentice-Hall.)"},{"key":"S0960129500000517_ref034","unstructured":"Isakowitz T. (1989) Theorem Proving Methods for Order Sorted Logic, Ph.D. thesis, University of Pennsylvania. (Also appeared in Logic in Computer Science \u201889 304\u2013312.)"},{"key":"S0960129500000517_ref007","unstructured":"Diaconescu R. (1992) The Formal Completeness of Equational Logics, Technical report PRG-TR- 12\u201392, Programming Research Group, Oxford University."},{"key":"S0960129500000517_ref009","first-page":"139","volume-title":"Proceedings, Ninth CAAP (Bordeaux","author":"Gogolla","year":"1984"},{"key":"S0960129500000517_ref031","volume-title":"Lectures on Boolean Algebras","author":"Halmos","year":"1963"},{"key":"S0960129500000517_ref011","unstructured":"Goguen J. (1978) Order Sorted Algebra, Technical Report 14, UCLA Computer Science Department (Semantics and Theory of Computation Series)."},{"key":"S0960129500000517_ref013","unstructured":"Goguen J. (1994) Theorem Proving and Algebra, MIT (to appear)."},{"key":"S0960129500000517_ref014","doi-asserted-by":"publisher","DOI":"10.1145\/147508.147524"},{"key":"S0960129500000517_ref019","first-page":"307","article-title":"Completeness of Many-sorted Equational Logic","volume":"11","author":"Goguen","year":"1985","journal-title":"Houston Journal of Mathematics"},{"key":"S0960129500000517_ref021","first-page":"66","article-title":"Remarks on Remarks on Many-Sorted Equational Logic","volume":"30","author":"Goguen","year":"1986","journal-title":"Bulletin of the European Association for Theoretical Computer Science"},{"key":"S0960129500000517_ref024","first-page":"417","volume-title":"Research Directions in Object-Oriented Programming","author":"Goguen","year":"1987"},{"key":"S0960129500000517_ref040","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030330"},{"key":"S0960129500000517_ref041","doi-asserted-by":"crossref","unstructured":"Poign\u00e9 A. (1990) Once More on Order-Sorted Algebra, Technical Report Draft, GMD.","DOI":"10.1007\/3-540-54345-7_83"},{"key":"S0960129500000517_ref025","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90302-V"},{"key":"S0960129500000517_ref027","unstructured":"Goguen J. , Thatcher J. and Wagner E. (1976) An Initial Algebra Approach to the Specification, Correctness and Implementation of Abstract Data Types. Technical Report RC 6487, IBM T. J. Watson Research Center. (Also in Yeh, R. (ed.) (1978) Current Trends in Programming Methodology, IV, Prentice-Hall 80\u2013149.)"},{"key":"S0960129500000517_ref029","volume-title":"Applications of Algebraic Specification using OBJ","author":"Goguen","year":"1994"},{"key":"S0960129500000517_ref035","doi-asserted-by":"publisher","DOI":"10.1073\/pnas.50.5.869"},{"key":"S0960129500000517_ref010","first-page":"234","volume-title":"Proceedings, First International Symposium on Category Theory Applied to Computation and Control","author":"Goguen","year":"1974"},{"key":"S0960129500000517_ref036","unstructured":"Meseguer J. and Goguen J. (1985) Deduction with Many-Sorted Rewrite Rules, Technical Report CSLI-85\u201342, Center for the Study of Language and Information, Stanford University. (To appear in Theoretical Computer Science.)"},{"key":"S0960129500000517_ref037","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028970"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129500000517","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,11]],"date-time":"2024-03-11T01:45:01Z","timestamp":1710121501000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129500000517\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994,9]]},"references-count":52,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1994,9]]}},"alternative-id":["S0960129500000517"],"URL":"https:\/\/doi.org\/10.1017\/s0960129500000517","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[1994,9]]}}}