{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:23:22Z","timestamp":1725665002261},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540626886"},{"type":"electronic","value":"9783540684381"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-62688-3_45","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T22:48:43Z","timestamp":1330296523000},"page":"336-353","source":"Crossref","is-referenced-by-count":1,"title":["Names, equations, relations: Practical ways to reason about new"],"prefix":"10.1007","author":[{"given":"Ian","family":"Stark","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"key":"21_CR1","unstructured":"S. Abramsky. The lazy lambda calculus. In Research Topics in Functional Programming, pages 65\u2013117. Addison Wesley, 1990."},{"key":"21_CR2","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1016\/0304-3975(92)90014-7","volume":"103","author":"M. Felleisen","year":"1992","unstructured":"M. Felleisen and R. Hieb. The revised report on the syntactic theories of sequential control and state. Theoretical Computer Science, 103:235\u2013271, 1992. Also published as Technical Report 100-89, Rice University.","journal-title":"Theoretical Computer Science"},{"key":"21_CR3","unstructured":"J. Frost and I. A. Mason. An operational logic of effects. In Computing: The Australasian Theory Symposium, Proceedings of CATS '96, pages 147\u2013156, January 1996."},{"key":"21_CR4","unstructured":"A. Gordon and A. Pitts, editors. Higher Order Operational Techniques in Semantics. Cambridge University Press, 1997. To appear."},{"key":"21_CR5","unstructured":"A. D. Gordon. Functional Programming and Input\/Output. Cambridge University Press, September 1994."},{"key":"21_CR6","doi-asserted-by":"crossref","unstructured":"A. D. Gordon. Bisimilarity as a theory of functional programming. In Mathematical Foundations of Programming Semantics: Proceedings of the 11th International Conference, Electronic Notes in Theoretical Computer Science 1. Elsevier, 1995.","DOI":"10.1016\/S1571-0661(04)80013-6"},{"issue":"1","key":"21_CR7","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1006\/inco.1995.1077","volume":"119","author":"F. Honsell","year":"1995","unstructured":"F. Honsell, I. A. Mason, S. Smith, and C. Talcott. A variable typed logic of effects. Information and Computation, 119(1):55\u201390, May 1995.","journal-title":"Information and Computation"},{"issue":"2","key":"21_CR8","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1006\/inco.1996.0008","volume":"124","author":"D. Howe","year":"1996","unstructured":"D. Howe. Proving congruence of bisimulation in functional programming languages. Information and Computation, 124(2):103\u2013112, February 1996.","journal-title":"Information and Computation"},{"key":"21_CR9","unstructured":"I. A. Mason. The Semantics of Destructive Lisp. PhD thesis, Stanford University, 1986. Also published as CSLI Lecture Notes Number 5, Center for the Study of Language and Information, Stanford University."},{"issue":"3","key":"21_CR10","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1017\/S0956796800000125","volume":"1","author":"I. A. Mason","year":"1991","unstructured":"I. A. Mason and C. Talcott. Equivalence in functional languages with effects. Journal of Functional Programming, 1(3):297\u2013327, July 1991.","journal-title":"Journal of Functional Programming"},{"key":"21_CR11","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. Talcott. Inferring the equivalence of functional programs that mutate data. Theoretical Computer Science, 105:167\u2013215, 1992.","journal-title":"Theoretical Computer Science"},{"key":"21_CR12","doi-asserted-by":"crossref","unstructured":"I. A. Mason and C. L. Talcott. References, local variables and operational reasoning. In Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science, pages 186\u2013197. IEEE Computer Society Press, 1992.","DOI":"10.1109\/LICS.1992.185532"},{"key":"21_CR13","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(77)90053-6","volume":"4","author":"R. Milner","year":"1977","unstructured":"R. Milner. Fully abstract models of typed \u03bb-calculi. Theoretical Computer Science, 4:1\u201322, 1977.","journal-title":"Theoretical Computer Science"},{"key":"21_CR14","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","volume":"100","author":"R. Milner","year":"1992","unstructured":"R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, parts I and II. Information and Computation, 100:1\u201377, 1992.","journal-title":"Information and Computation"},{"key":"21_CR15","unstructured":"R. Milner, M. Tofte, and R. Harper. The Definition of Standard ML. MIT Press, 1990."},{"issue":"1","key":"21_CR16","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1016\/0890-5401(91)90052-4","volume":"93","author":"E. Moggi","year":"1991","unstructured":"E. Moggi. Notions of computation and monads. Information and Computation, 93(1):55\u201392, July 1991.","journal-title":"Information and Computation"},{"key":"21_CR17","doi-asserted-by":"crossref","unstructured":"E. Moggi. A general semantics for evaluation logic. In Proceedings of the Ninth Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, 1994.","DOI":"10.1109\/LICS.1994.316054"},{"key":"21_CR18","unstructured":"E. Moggi. Representing program logics in evaluation logic. Unpublished manuscript, available electronically, 1994."},{"key":"21_CR19","doi-asserted-by":"crossref","unstructured":"L. C. Paulson. Isabelle: A Generic Theorem Prover. Lecture Notes in Computer Science 828. Springer-Verlag, 1994.","DOI":"10.1007\/BFb0030541"},{"key":"21_CR20","unstructured":"A. Pitts and I. Stark. Operational reasoning for functions with local state. In Gordon and Pitts [4]. To appear."},{"key":"21_CR21","doi-asserted-by":"crossref","unstructured":"A. M. Pitts. Evaluation logic. In IVth Higher Order Workshop, Banff 1990, pages 162\u2013189. Springer-Verlag, 1991. Also published as Technical Report 198, University of Cambridge Computer Laboratory.","DOI":"10.1007\/978-1-4471-3182-3_11"},{"key":"21_CR22","doi-asserted-by":"crossref","unstructured":"A. M. Pitts and I. Stark. Observable properties of higher order functions that dynamically create local names, or: What's new? In Mathematical Foundations of Computer Science: Proceedings of the 18th International Symposium, Lecture Notes in Computer Science 711, pages 122\u2013141. Springer-Verlag, 1993.","DOI":"10.1007\/3-540-57182-5_8"},{"key":"21_CR23","unstructured":"A. M. Pitts and I. Stark. On the observable properties of higher order functions that dynamically create local names (preliminary report). In Proceedings of the 1993 ACM SIGPLAN Workshop on State in Programming Languages, Yale University Department of Computer Science, Research Report YALEU\/DCS\/RR-968, pages 31\u201345, 1993."},{"key":"21_CR24","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 \u03bb-calculus. Theoretical Computer Science, 1:125\u2013159, 1975.","journal-title":"Theoretical Computer Science"},{"issue":"3\/4","key":"21_CR25","first-page":"287","volume":"6","author":"A. Sabry","year":"1993","unstructured":"A. Sabry and M. Felleisen. Reasoning about programs in continuation-passing style. Lisp and Symbolic Computation, 6(3\/4):287\u2013358, 1993.","journal-title":"Lisp and Symbolic Computation"},{"key":"21_CR26","unstructured":"I. Stark. Names and Higher-Order Functions. PhD thesis, University of Cambridge, December 1994. Also published as Technical Report 363, University of Cambridge Computer Laboratory."},{"issue":"1","key":"21_CR27","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1007\/BF01806033","volume":"9","author":"I. Stark","year":"1996","unstructured":"I. Stark. Categorical models for local names. Lisp and Symbolic Computation, 9(1):77\u2013107, February 1996.","journal-title":"Lisp and Symbolic Computation"},{"key":"21_CR28","unstructured":"C. Talcott. Reasoning about functions with effects. In Gordon and Pitts [4]. To appear."}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-62688-3_45.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:14:05Z","timestamp":1605647645000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-62688-3_45"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540626886","9783540684381"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/3-540-62688-3_45","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}