{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:28:20Z","timestamp":1761611300615},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540569923"},{"type":"electronic","value":"9783540478904"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/3-540-56992-8_18","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T06:59:56Z","timestamp":1330239596000},"page":"309-326","source":"Crossref","is-referenced-by-count":1,"title":["A theory of classes for a functional language with effects"],"prefix":"10.1007","author":[{"given":"Furio","family":"Honsell","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ian A.","family":"Mason","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Scott","family":"Smith","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carolyn","family":"Talcott","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"issue":"1","key":"18_CR1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1142\/S0129054191000029","volume":"2","author":"M. Abadi","year":"1991","unstructured":"M. Abadi, B. Pierce, and G. Plotkin. Faithful ideal models for recursive polymorphic types. International Journal of Foundations of Computer Science, 2(1):1\u201321, 1991.","journal-title":"International Journal of Foundations of Computer Science"},{"key":"18_CR2","doi-asserted-by":"crossref","unstructured":"S. Feferman. A language and axioms for explicit mathematics. In Algebra and Logic, volume 450 of Springer Lecture Notes in Mathematics, pages 87\u2013139. Springer Verlag, 1975.","DOI":"10.1007\/BFb0062852"},{"key":"18_CR3","first-page":"95","volume":"19","author":"S. Feferman","year":"1985","unstructured":"S. Feferman. A theory of variable types. Revista Colombiana de Mat\u00e9maticas, 19:95\u2013105, 1985.","journal-title":"Revista Colombiana de Mat\u00e9maticas"},{"key":"18_CR4","doi-asserted-by":"crossref","unstructured":"S. Feferman. Polymorphic typed lambda-calculi in a type-free axiomatic framework. In Logic and Computation, volume 106 of Contemporary Mathematics, pages 101\u2013136. A.M.S., Providence R. I., 1990.","DOI":"10.1090\/conm\/106\/1057818"},{"key":"18_CR5","unstructured":"M. Felleisen. The Calculi of Lambda-v-cs Conversion: A Syntactic Theory of Control and State in Imperative Higher-Order Programming Languages. PhD thesis, Indiana University, 1987."},{"key":"18_CR6","unstructured":"M. Felleisen and A. K. Wright. A syntactic approach to type soundness. Technical Report Rice COMP TR91-160, Rice University Computer Science Department, 1991."},{"key":"18_CR7","doi-asserted-by":"crossref","unstructured":"J.Y. Halpern, A. R. Meyer, and B. A. Trakhtenbrot. The semantics of local storage, or what makes the free-list free? In 11th ACM Symposium on Principles of Programming Languages, pages 245\u2013257, 1983.","DOI":"10.1145\/800017.800536"},{"key":"18_CR8","volume-title":"Logics of Programs, Proceedings 1983, volume 164 of Lecture Notes in Computer Science","author":"J.Y. Halpern","year":"1984","unstructured":"J.Y. Halpern, A. R. Meyer, and B. A. Trakhtenbrot. From denotational to operational and axiomatic semantics for ALGOL-like languages: An overview. In E. Clarke and D. Kozen, editors, Logics of Programs, Proceedings 1983, volume 164 of Lecture Notes in Computer Science. Springer, Berlin, 1984."},{"key":"18_CR9","doi-asserted-by":"crossref","unstructured":"X. Leroy and P. Wies. Polymorphic type inference and assignment. In Proceedings of the 18th Annual Symposium on Principles of Programming Languages, pages 291\u2013302. ACM, 1990.","DOI":"10.1145\/99583.99622"},{"key":"18_CR10","unstructured":"J. M. Lucassen. Types and Effects, towards the integration of functional and imperative programming. PhD thesis, MIT, 1987. Also available as LCS TR-408."},{"key":"18_CR11","doi-asserted-by":"crossref","unstructured":"J. M. Lucassen and D. K. Gifford. Polymorphic effect systems. In 16th annual ACM Symposium on Principles of Programming Languages, pages 47\u201357, 1988.","DOI":"10.1145\/73560.73564"},{"key":"18_CR12","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1007\/BF00264494","volume":"16","author":"Z. Manna","year":"1981","unstructured":"Z. Manna and R Waldinger. Problematic features of programming languages. Acta Informatica, 16:371\u2013426, 1981.","journal-title":"Acta Informatica"},{"key":"18_CR13","doi-asserted-by":"crossref","unstructured":"I. A. Mason and C. L. Talcott. Axiomatizing operational equivalence in the presence of side effects. In Fourth Annual Symposium on Logic in Computer Science. IEEE, 1989.","DOI":"10.1109\/LICS.1989.39183"},{"key":"18_CR14","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1017\/S0956796800000125","volume":"1","author":"I. A. Mason","year":"1991","unstructured":"I. A. Mason and C. L. Talcott. Equivalence in functional languages with effects. Journal of Functional Programming, 1:287\u2013327, 1991.","journal-title":"Journal of Functional Programming"},{"issue":"2","key":"18_CR15","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1016\/0304-3975(92)90301-U","volume":"105","author":"I. A. Mason","year":"1992","unstructured":"I. A. Mason and C. L. Talcott. Inferring the equivalence of functional programs that mutate data. Theoretical Computer Science, 105(2):167\u2013215, 1992.","journal-title":"Theoretical Computer Science"},{"key":"18_CR16","doi-asserted-by":"crossref","unstructured":"I. A. Mason and C. L. Talcott. References, local variables and operational reasoning. In Seventh Annual Symposium on Logic in Computer Science, pages 186\u2013197. IEEE, 1992.","DOI":"10.1109\/LICS.1992.185532"},{"key":"18_CR17","doi-asserted-by":"crossref","unstructured":"A. R. Meyer and K. Sieber. Towards fully abstract semantics for local variables: Preliminary report. In 15th ACM Symposium on Principles of Programming Languages, pages 191\u2013208, 1988.","DOI":"10.1145\/73560.73577"},{"key":"18_CR18","doi-asserted-by":"crossref","unstructured":"E. Moggi. Computational lambda-calculus and monads. In Fourth Annual Symposium on Logic in Computer Science. IEEE, 1989.","DOI":"10.1109\/LICS.1989.39155"},{"key":"18_CR19","unstructured":"J. H. Morris. Lambda calculus models of programming languages. PhD thesis, Massachusetts Institute of Technology, 1968."},{"key":"18_CR20","unstructured":"P.W. O'Hearn and R.D. Tennent. Semantic Analysis of Specification Logic, Part 2. Information and Computation, ?:?-?, 199?"},{"key":"18_CR21","doi-asserted-by":"crossref","unstructured":"P.W. O'Hearn and R.D. Tennent. Semantics of Local Variables. Technical Report ECS-LFCS-92-192, Laboratory for foundations of computer science, University of Edinburgh, 1992.","DOI":"10.1017\/CBO9780511525902.013"},{"key":"18_CR22","volume-title":"Logics of Programs, Proceedings 1983, volume 164 of Lecture Notes in Computer Science","author":"E. Olderog","year":"1984","unstructured":"E. Olderog. Hoare's logic for programs with procedures-what has been accomplished. In E. Clarke and D. Kozen, editors, Logics of Programs, Proceedings 1983, volume 164 of Lecture Notes in Computer Science. Springer, Berlin, 1984."},{"key":"18_CR23","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/0304-3975(75)90017-1","volume":"1","author":"G. Plotkin","year":"1975","unstructured":"G. Plotkin. Call-by-name, call-by-value and the lambda-v-calculus. Theoretical Computer Science, 1:125\u2013159, 1975.","journal-title":"Theoretical Computer Science"},{"key":"18_CR24","doi-asserted-by":"crossref","unstructured":"J. C. Reynolds. Syntactic control of interference. In Conference record of the 5th annual ACM Symposium on Principles of Programming Languages, pages 39\u20136, 1978.","DOI":"10.1145\/512760.512766"},{"key":"18_CR25","volume-title":"Logics of Programs, volume 193 of Lecture Notes in Computer Science","author":"K. Sieber","year":"1985","unstructured":"K. Sieber. A partial correctness logic for programs (in an Algol-like language). In R. Parikh, editor, Logics of Programs, volume 193 of Lecture Notes in Computer Science. Springer, Berlin, 1985."},{"key":"18_CR26","unstructured":"Scott Fraser Smith. Partial objects in type theory. Technical Report TR 88-938, Department of Computer Science, Cornell University, 1988. Ph. D. thesis."},{"key":"18_CR27","doi-asserted-by":"crossref","unstructured":"C. L. Talcott. A theory for program and data specification. In Design and Implementation of Symbolic Computation Systems, DISCO'90, volume 429 of Lecture Notes in Computer Science, pages 91\u2013100. Springer-Verlag, 1990. Full version to appear in TCS special issue.","DOI":"10.1007\/3-540-52531-9_128"},{"key":"18_CR28","unstructured":"M. Tofte. Operational Semantics and Polymorphic Type Inference. PhD thesis, Edinburgh University, 1988."},{"key":"18_CR29","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0890-5401(90)90018-D","volume":"89","author":"M. Tofte","year":"1990","unstructured":"M. Tofte. Type inference for polymorphic references. Information and Computation, 89:1\u201334, 1990.","journal-title":"Information and Computation"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-56992-8_18.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,31]],"date-time":"2021-12-31T00:10:47Z","timestamp":1640909447000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-56992-8_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"ISBN":["9783540569923","9783540478904"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/3-540-56992-8_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1993]]}}}