{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:22:30Z","timestamp":1725456150450},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540600176"},{"type":"electronic","value":"9783540494041"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/bfb0022269","type":"book-chapter","created":{"date-parts":[[2005,11,22]],"date-time":"2005-11-22T06:12:29Z","timestamp":1132639949000},"page":"369-381","source":"Crossref","is-referenced-by-count":3,"title":["Towards machine-checked compiler correctness for higher-order pure functional languages"],"prefix":"10.1007","author":[{"given":"David","family":"Lester","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sava","family":"Mintchev","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,15]]},"reference":[{"key":"27_CR1","unstructured":"A. Cohn. The equivalence of two semantic definitions: a case study in LCF. Technical Report CSR-76-81, Department of Computer Science, Edinburgh University, January 1981."},{"issue":"1\/2","key":"27_CR2","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/BF01383985","volume":"3","author":"P. Curzon","year":"1993","unstructured":"P. Curzon. Deriving correctness properties of compiled code. Formal Methods in System Design, 3(1\/2):83\u2013115, August 1993.","journal-title":"Formal Methods in System Design"},{"key":"27_CR3","doi-asserted-by":"crossref","unstructured":"D.R. Lester. The G-machine as a representation of stack semantics. In G. Kahn, editor, Proceedings of the Functional Programming Languages and Computer Architecture Conference, pages 46\u201359. Springer-Verlag LNCS 274, September 1987.","DOI":"10.1007\/3-540-18317-5_4"},{"key":"27_CR4","unstructured":"D.R. Lester. Combinator Graph Reduction: A Congruence and its Applications. Dphil thesis, Oxford University, 1988. Also published as Technical Monograph PRG-73."},{"key":"27_CR5","unstructured":"R.E. Milne. The Formal Semantics of Computer Languages and Their Implementation. PhD thesis, University of Cambridge, 1974."},{"key":"27_CR6","unstructured":"P.D. Mosses. SIS \u2014 semantics implementation system. Technical Report DAIMI MD-30, Computer Science Department, Aarhus University, 1979."},{"key":"27_CR7","volume-title":"ACM Doctoral Dissertation Award 1986","author":"K. Mulmuley","year":"1987","unstructured":"K. Mulmuley. Full Abstraction and Semantic Equivalence. MIT Press, Cambridge, Massachusetts, 1987. ACM Doctoral Dissertation Award 1986."},{"key":"27_CR8","doi-asserted-by":"crossref","unstructured":"F. Nielson and H.R. Nielson. Two-level Functional Languages. Number 34 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1992.","DOI":"10.1017\/CBO9780511526572"},{"key":"27_CR9","doi-asserted-by":"crossref","unstructured":"J. Palsberg. A Provably Correct Compiler Generator. PhD thesis, Computer Science Department, Aarhus University, January 1992. Also published as Technical Report DAIMI PB-382.","DOI":"10.7146\/dpb.v21i382.6614"},{"key":"27_CR10","doi-asserted-by":"crossref","unstructured":"L.C. Paulson. A semantics-directed compiler generator. In Ninth Symposium on Principles of Programming Languages, pages 224\u2013233, 1982.","DOI":"10.1145\/582153.582178"},{"key":"27_CR11","doi-asserted-by":"crossref","unstructured":"L.C. Paulson. Logic and Computation: Interactive proof with Cambridge LCF. Cambridge University Press, 1987.","DOI":"10.1017\/CBO9780511526602"},{"key":"27_CR12","unstructured":"L.C. Paulson. Introduction to Isabelle. Technical report, Computer Laboratory, University of Cambridge, 1992."},{"key":"27_CR13","first-page":"86","volume-title":"Relational properties of recursively defined domains","author":"A.M. Pitts","year":"1993","unstructured":"A.M. Pitts. Relational properties of recursively defined domains. In Proc. 8th Annual Symposium on Logic in Computer Science, pages 86\u201397, Washington, 1993. IEEE Computer Soc. Press."},{"key":"27_CR14","first-page":"141","volume-title":"On the relation between direct and continuation semantics","author":"J.C. Reynolds","year":"1974","unstructured":"J.C. Reynolds. On the relation between direct and continuation semantics. In Proceedings of the Second Colloquium on Automata, Languages and Programming, pages 141\u2013156, Saarbrucken, 1974. Springer-Verlag."},{"key":"27_CR15","series-title":"The MIT Press Series in Computer Science","volume-title":"Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory","author":"J.E. Stoy","year":"1977","unstructured":"J.E. Stoy. Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. The MIT Press Series in Computer Science. MIT Press, Cambridge, Massachusetts, 1977."},{"issue":"2","key":"27_CR16","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1016\/0304-3975(81)90037-2","volume":"13","author":"J.E. Stoy","year":"1981","unstructured":"J.E. Stoy. The congruence of two programming language definitions. Theoretical Computer Science, 13(2):151\u2013174, February 1981.","journal-title":"Theoretical Computer Science"},{"key":"27_CR17","series-title":"NATO Advanced Study Institute Series, C91","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1007\/978-94-009-7893-5_10","volume-title":"Theoretical Foundations of Programming Methodology. Lecture notes of an International Summer School","author":"J.E. Stoy","year":"1982","unstructured":"J.E. Stoy. Semantic models. In M. Broy and G. Schmidt, editors, Theoretical Foundations of Programming Methodology. Lecture notes of an International Summer School, directed by F.L. Bauer, E.W. Dijkstra and C.A.R. Hoare, pages 293\u2013324, Boston, Massachusetts, 1982. NATO Advanced Study Institute Series, C91, D. Reidel Publishing Co."},{"key":"27_CR18","first-page":"217","volume-title":"Functional Programming and its Applications: An Advanced Course","author":"J.E. Stoy","year":"1982","unstructured":"J.E. Stoy. Some mathematical aspects of functional programming. In J. Darlington, P. Henderson, and D.A. Turner, editors, Functional Programming and its Applications: An Advanced Course, pages 217\u2013252. Cambridge University Press, Cambridge, England, 1982."},{"issue":"3","key":"27_CR19","doi-asserted-by":"publisher","first-page":"496","DOI":"10.1145\/357172.357179","volume":"4","author":"M. Wand","year":"1982","unstructured":"M. Wand. Deriving target code as a representation of continuation semantics. ACM Transactions on Programming Languages and Systems, 4(3):496\u2013517, July 1982.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"27_CR20","doi-asserted-by":"crossref","unstructured":"M. Wand. A semantic prototyping system. In Proceedings of the ACM SIGPLAN'84 Symposium on Compiler Construction, pages 213\u2013221, 1984.","DOI":"10.1145\/502874.502895"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0022269","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T02:43:08Z","timestamp":1586572988000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0022269"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540600176","9783540494041"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/bfb0022269","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}