{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T13:59:43Z","timestamp":1754488783901,"version":"3.40.4"},"reference-count":10,"publisher":"Elsevier","isbn-type":[{"type":"print","value":"9780124500105"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1991]]},"DOI":"10.1016\/b978-0-12-450010-5.50007-4","type":"book-chapter","created":{"date-parts":[[2012,12,3]],"date-time":"2012-12-03T06:21:49Z","timestamp":1354515709000},"page":"7-26","source":"Crossref","is-referenced-by-count":27,"title":["Functional Instantiation in First-Order Logic"],"prefix":"10.1016","author":[{"given":"Robert S.","family":"Boyer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David M.","family":"Goldschlag","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matt","family":"Kaufmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J. Strother","family":"Moore","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/B978-0-12-450010-5.50007-4_bib1","unstructured":"Robert S. Boyer, David M. Goldschlag, Matt Kaufmann, and J Strother Moore. Functional Instantiation in First-Order Logic. Technical Report 44, Computational Logic, Inc., Austin, Texas. Extended version of this chapter."},{"year":"1988","series-title":"A Computational Logic Handbook","author":"Boyer","key":"10.1016\/B978-0-12-450010-5.50007-4_bib2"},{"key":"10.1016\/B978-0-12-450010-5.50007-4_bib3","series-title":"The Correctness Problem in Computer Science","article-title":"An Informal Introduction to Specification Using Clear","author":"Burstall","year":"1981"},{"key":"10.1016\/B978-0-12-450010-5.50007-4_bib4","series-title":"Programming Concepts and Methods","article-title":"Mechanizing Unity","author":"Goldschlag","year":"1990"},{"year":"1964","series-title":"Recursive Number Theory","author":"Goodstein","key":"10.1016\/B978-0-12-450010-5.50007-4_bib5"},{"key":"10.1016\/B978-0-12-450010-5.50007-4_ceotherref2","doi-asserted-by":"crossref","unstructured":"John McCarthy. A Basis for Mathematical Theory of Computation. In Proc. Western Joint Computer Conf., pages 225\u2013238, May 1961. Later version in","DOI":"10.1145\/1460690.1460715"},{"first-page":"33","year":"1963","series-title":"Computer Programming and Formal Systems","key":"10.1016\/B978-0-12-450010-5.50007-4_sbref5"},{"key":"10.1016\/B978-0-12-450010-5.50007-4_bib7","unstructured":"J S. Moore. Piton: A Verified Assembly Level Language. Technical Report 22, Computational Logic, Inc., Austin, TX, 1988."},{"issue":"4","key":"10.1016\/B978-0-12-450010-5.50007-4_bib8","doi-asserted-by":"crossref","first-page":"461","DOI":"10.1007\/BF00243133","article-title":"A Mechanically Verified Language Implementation","volume":"5","author":"Moore","year":"1989","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-0-12-450010-5.50007-4_bib9","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1002\/spe.4380090105","article-title":"A New Implementation Technique for Applicative Languages","volume":"9","author":"Turner","year":"1979","journal-title":"Software \u2013 Practice and Experience"}],"container-title":["Artificial and Mathematical Theory of Computation"],"original-title":[],"language":"en","deposited":{"date-parts":[[2025,4,23]],"date-time":"2025-04-23T02:50:53Z","timestamp":1745376653000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/B9780124500105500074"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991]]},"ISBN":["9780124500105"],"references-count":10,"URL":"https:\/\/doi.org\/10.1016\/b978-0-12-450010-5.50007-4","relation":{},"subject":[],"published":{"date-parts":[[1991]]}}}