{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:36:41Z","timestamp":1725457001564},"publisher-location":"Berlin\/Heidelberg","reference-count":26,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"3540528261"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0032019","type":"book-chapter","created":{"date-parts":[[2005,12,11]],"date-time":"2005-12-11T06:05:31Z","timestamp":1134281131000},"page":"20-31","source":"Crossref","is-referenced-by-count":1,"title":["A complete and decidable proof system for call-by-value equalities"],"prefix":"10.1007","author":[{"given":"Jon G.","family":"Riecke","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"3_CR1","unstructured":"Harold Abelson and Gerald Jay Sussman. Structure and Interpretation of Computer Programs. MIT Press and McGraw-Hill, 1985."},{"key":"3_CR2","unstructured":"Henk P. Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic. North-Holland, 1981. Revised Edition, 1984."},{"key":"3_CR3","unstructured":"Stavros S. Cosmadakis, Albert R. Meyer, and Jon G. Riecke. Completeness for typed lazy inequalities (preliminary report). In 5 th Symp. Logic in Computer Science. IEEE, 1990. To appear."},{"key":"3_CR4","first-page":"50","volume":"80","author":"P.-L. Curien","year":"1989","unstructured":"P.-L. Curien and A. Obtu\u0142owicz. Partiality, cartesian closedness, and toposes. Information and Control, 80:50\u201395, 1989.","journal-title":"Information and Control"},{"key":"3_CR5","unstructured":"Herbert B. Enderton. A Mathematical Introduction to Logic. Academic Press, 1972."},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Harvey Friedman. Equality between functionals. In Rohit Parikh, editor, Logic Colloquium '73, volume 453 of Lect. Notes in Math., pages 22\u201337. Springer-Verlag, 1975.","DOI":"10.1007\/BFb0064870"},{"key":"3_CR7","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1016\/S0019-9958(82)80087-9","volume":"52","author":"A. R. Meyer","year":"1982","unstructured":"Albert R. Meyer. What is a model of the lambda calculus? Information and Control, 52:87\u2013122, 1982.","journal-title":"Information and Control"},{"key":"3_CR8","unstructured":"Robin Milner. A proposal for Standard ML. Polymorphism, 1(3), December 1983."},{"key":"3_CR9","series-title":"Lect. Notes in Computer Sci.","volume-title":"Categories of partial morphisms and the \u03bb p -calculus","author":"E. Moggi","year":"1986","unstructured":"Eugenio Moggi. Categories of partial morphisms and the \u03bb p -calculus. In Proceedings of Workshop on Category Theory and Computer Programming, Guildford, 1985, volume 240 of Lect. Notes in Computer Sci., New York, 1986. Springer-Verlag."},{"key":"3_CR10","unstructured":"Eugenio Moggi. The Partial Lambda Calculus. PhD thesis, University of Edinburgh, 1988."},{"key":"3_CR11","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/0304-3975(75)90017-1","volume":"1","author":"G. D. Plotkin","year":"1975","unstructured":"Gordon D. Plotkin. Call-by-name, call-by-value and the \u03bb-calculus. Theoretical Computer Sci., 1:125\u2013159, 1975.","journal-title":"Theoretical Computer Sci."},{"key":"3_CR12","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1016\/0304-3975(77)90044-5","volume":"5","author":"G. D. Plotkin","year":"1977","unstructured":"Gordon D. Plotkin. LCF considered as a programming language. Theoretical Computer Sci., 5:223\u2013257, 1977.","journal-title":"Theoretical Computer Sci."},{"key":"3_CR13","series-title":"Technical Report","volume-title":"A structural approach to operational semantics","author":"G. D. Plotkin","year":"1981","unstructured":"Gordon D. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Aarhus Univ., Computer Science Dept., Denmark, 1981."},{"key":"3_CR14","unstructured":"Gordon D. Plotkin. Notes on completeness of the full continuous type hierarchy. Unpublished manuscript, MIT, November 1982."},{"key":"3_CR15","unstructured":"Gordon D. Plotkin. (Towards a) logic for computable functions. Unpublished manuscript, CSLI Summer School Notes, 1985."},{"key":"3_CR16","unstructured":"G. Rosolini. Continuity and Effectiveness in Topoi. PhD thesis, Oxford University, 1986."},{"key":"3_CR17","doi-asserted-by":"crossref","first-page":"308","DOI":"10.1007\/BF01876321","volume":"15","author":"V. Sazonov","year":"1976","unstructured":"V.Yu. Sazonov. Expressibility of functions in D. Scott's LCF language. Algebra i Logika, 15:308\u2013330, 1976. (Russian).","journal-title":"Algebra i Logika"},{"key":"3_CR18","unstructured":"Dana Scott. A type theoretical alternative to CUCH, ISWIM, OWHY. Oxford University, unpublished manuscript, 1969."},{"key":"3_CR19","doi-asserted-by":"crossref","first-page":"522","DOI":"10.1137\/0205037","volume":"5","author":"D. Scott","year":"1976","unstructured":"Dana Scott. Data types as lattices. SIAM J. Computing, 5:522\u2013587, 1976.","journal-title":"SIAM J. Computing"},{"key":"3_CR20","unstructured":"Kurt Sieber. Message to the types@theory.lcs.mit.edu electronic mail forum, June 1989."},{"key":"3_CR21","unstructured":"Kurt Sieber. Personal communication, January 1990."},{"key":"3_CR22","doi-asserted-by":"crossref","unstructured":"Dorai Sitaram and Matthias Felleisen. Reasoning with continuations II: Full abstraction for models of control. In Proc. Conf. LISP and Functional Programming. ACM, 1990. To appear.","DOI":"10.1145\/91556.91626"},{"key":"3_CR23","doi-asserted-by":"crossref","unstructured":"Richard Statman. Equality between functionals revisited. In L.A. Harrington, et al., editor, Harvey Friedman's Research on the Foundations of Mathematics, volume 117 of Studies in Logic, pages 331\u2013338. North-Holland, 1985.","DOI":"10.1016\/S0049-237X(09)70166-1"},{"key":"3_CR24","doi-asserted-by":"crossref","first-page":"86","DOI":"10.1016\/S0019-9958(85)80001-2","volume":"65","author":"R. Statman","year":"1985","unstructured":"Richard Statman. Logical relations in the typed \u03bb-calculus. Information and Control, 65:86\u201397, 1985.","journal-title":"Information and Control"},{"key":"3_CR25","volume-title":"Common Lisp: The Language","author":"G. L. Steele","year":"1984","unstructured":"Guy L. Steele. Common Lisp: The Language. Digital Press, Bedford, MA, 1984."},{"issue":"3","key":"3_CR26","doi-asserted-by":"crossref","first-page":"488","DOI":"10.1137\/0205036","volume":"5","author":"C. P. Wadsworth","year":"1976","unstructured":"Christopher P. Wadsworth. The relation between computational and denotational properties for Scott's D\u221e models. SIAM J. Computing, 5(3):488\u2013521, 1976.","journal-title":"SIAM J. Computing"}],"container-title":["Lecture Notes in Computer Science","Automata, Languages and Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/www.springerlink.com\/index\/pdf\/10.1007\/BFb0032019","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T13:45:42Z","timestamp":1586612742000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0032019"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540528261"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/bfb0032019","relation":{},"subject":[]}}