{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:03:29Z","timestamp":1725663809869},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540578260"},{"type":"electronic","value":"9783540483465"}],"license":[{"start":{"date-parts":[[1994,1,1]],"date-time":"1994-01-01T00:00:00Z","timestamp":757382400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-57826-9_122","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T08:26:24Z","timestamp":1330244784000},"page":"16-28","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Graph model of LAMBDA in higher order logic"],"prefix":"10.1007","author":[{"given":"Kim Dam","family":"Petersen","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"Sten Agerholm. Formalising Domain Theory in HOL. Computer Science Department, Aarhus University. DRAFT, March, 1993.","DOI":"10.1007\/3-540-57826-9_143"},{"key":"2_CR2","unstructured":"Hendrik P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North Holland, 1984."},{"key":"2_CR3","unstructured":"R. S. Boyer and J. S. Moore. A Computational Logic. Academic Press, 1979."},{"key":"2_CR4","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"Alonzo Church. A Formulation of the Simple Theory of Types. Journal of Symbolic Logic, Vol. 5 (1940), pp. 56\u201368.","journal-title":"Journal of Symbolic Logic"},{"key":"2_CR5","unstructured":"Anders Gammelgaard and Kim D. Petersen. Unpublished note."},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"Elsa L. Gunter. Why we can't have SML Style datatype Declarations in HOL. Proceedings from International Workshop on Higher Order Logic Theorem Proving and its Applications, 1992.","DOI":"10.1016\/B978-0-444-89880-7.50042-5"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"Mike J. Gordon. HOL \u2014 A Proof Generating System for Higher-Order Logic. VLSI Specification, Verification and Synthesis, Kluwer, 1987.","DOI":"10.1007\/978-1-4613-2007-4_3"},{"key":"2_CR8","unstructured":"The HOL System: DESCRIPTION, Version HOL88.2.01 (1992). HOL88 documentation."},{"key":"2_CR9","unstructured":"Larry C. Paulson and Tobias Nipkow. Isabelle Tutorial and User's Manual. Unpublished, Isabelle documentation, 1988."},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"Mike J. Gordon, Robin Milner and Christopher P. Wadsworth. Edinburgh LCF: A Mechanised Logic of Computation. LNCS 78, Springer Verlag, 1979.","DOI":"10.1007\/3-540-09724-4"},{"key":"2_CR11","unstructured":"David Schmidt. Denotational Semantics: A Methodology for Language Development. Allyn and Bacon, 1986."},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"Dana Scott. Data Types as Lattices. SIAM J. Comput. Vol. 5, No. 3, September 1976.","DOI":"10.1137\/0205037"},{"key":"2_CR13","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/3054.001.0001","volume-title":"The Formal Semantics of Programming Languages","author":"G. Winskel","year":"1993","unstructured":"Glynn Winskel. The Formal Semantics of Programming Languages. MIT Press, Cambridge, 1993."}],"container-title":["Lecture Notes in Computer Science","Higher Order Logic Theorem Proving and Its Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-57826-9_122","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,8]],"date-time":"2020-01-08T19:08:57Z","timestamp":1578510537000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-57826-9_122"}},"subtitle":["Progress report"],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540578260","9783540483465"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-57826-9_122","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]},"assertion":[{"value":"31 May 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}