{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:11:00Z","timestamp":1725664260011},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540580850"},{"type":"electronic","value":"9783540484400"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58085-9_85","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T15:11:06Z","timestamp":1330269066000},"page":"366-383","source":"Crossref","is-referenced-by-count":0,"title":["Semantics for abstract clauses"],"prefix":"10.1007","author":[{"given":"D. A.","family":"Wolfram","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"17_CR1","doi-asserted-by":"crossref","first-page":"739","DOI":"10.1016\/S0049-237X(08)71120-0","volume-title":"Handbook of Mathematical Logic","author":"P. Aczel","year":"1977","unstructured":"P. Aczel, An introduction to inductive definitions, in: Handbook of Mathematical Logic, (J. Barwise, Ed.), North-Holland, Amsterdam, 1977, 739\u2013782."},{"key":"17_CR2","volume-title":"An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof","author":"P.B. Andrews","year":"1986","unstructured":"P.B. Andrews, An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, Academic, Orlando, 1986."},{"key":"17_CR3","volume-title":"The Lambda-Calculus: Its Syntax and Semantics, Volume II","author":"H.P. Barendregt","year":"1984","unstructured":"H.P. Barendregt, The Lambda-Calculus: Its Syntax and Semantics, Volume II, Second Edition, North-Holland, Amsterdam, 1984.","edition":"Second Edition"},{"issue":"2\/3","key":"17_CR4","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"1988","unstructured":"Th. Coquand and G. Huet, The Calculus of Constructions, Information and Computation 76, 2\/3 (1988) 95\u2013120.","journal-title":"Information and Computation"},{"key":"17_CR5","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/321978.321991","volume":"24","author":"M.H. Emden van","year":"1976","unstructured":"M.H. van Emden and R.A. Kowalski, The semantics of predicate logic as a programming language, Journal of the Association for Computing Machinery 24 (1976) 733\u2013742.","journal-title":"Journal of the Association for Computing Machinery"},{"issue":"1","key":"17_CR6","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1983","unstructured":"R. Harper, F. Honsell, and G. Plotkin, A framework for defining logics, Journal of the Association for Computing Machinery 40, 1 (1983) 143\u2013184.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"17_CR7","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"G.P. Huet","year":"1975","unstructured":"G.P. Huet, A unification algorithm for typed \u03bb-calculus, Theoretical Computer Science 1 (1975) 27\u201357.","journal-title":"Theoretical Computer Science"},{"key":"17_CR8","volume-title":"Th\u00e8se de Doctorat d'Etat","author":"G.P. Huet","year":"1976","unstructured":"G.P. Huet, R\u00e9solution d'\u00e9quations dans des Langages d'Ordre 1,2,...,\u03c9, Th\u00e8se de Doctorat d'Etat, Universit\u00e9 Paris VII, Paris, 1976."},{"key":"17_CR9","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1090\/conm\/092\/1003199","volume":"92","author":"J.M.E. Hyland","year":"1989","unstructured":"J.M.E. Hyland and A.M. Pitts, The Theory of Constructions: categorical semantics and topos-theoretic models, Contemporary Mathematics 92 (1989) 137\u2013199.","journal-title":"Contemporary Mathematics"},{"key":"17_CR10","volume-title":"Introduction to Metamathematics","author":"S.C. Kleene","year":"1952","unstructured":"S.C. Kleene, Introduction to Metamathematics, Van Nostrand, Princeton, 1952."},{"key":"17_CR11","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/BF00248324","volume":"5","author":"L.C. Paulson","year":"1989","unstructured":"L.C. Paulson, The foundation of a generic theorem prover, Journal of Automated Reasoning 5 (1989) 363\u2013397.","journal-title":"Journal of Automated Reasoning"},{"key":"17_CR12","first-page":"361","volume-title":"Logic and Computer Science","author":"L.C. Paulson","year":"1990","unstructured":"L.C. Paulson, Isabelle: the next 700 theorem provers, In Logic and Computer Science, (P. Oddifreddi, Ed.), Academic, Orlando, 1990, 361\u2013386."},{"key":"17_CR13","doi-asserted-by":"crossref","unstructured":"F. Pfenning, Logic programming in the LF logical framework, in: Logical Frame-works, (G. Huet and G. Plotkin, Eds.), Cambridge, 1991, 149\u2013181.","DOI":"10.1017\/CBO9780511569807.008"},{"key":"17_CR14","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A. Tarski","year":"1955","unstructured":"A. Tarski, A lattice-theoretical fixpoint theorem and its applications, Pacific Journal of Mathematics 5 (1955) 285\u2013309.","journal-title":"Pacific Journal of Mathematics"},{"key":"17_CR15","unstructured":"D.A. Wolfram, M.J. Maher, and J-L. Lassez, A unified treatment of resolution strategies for logic programs, Proceedings of the Second International Logic Programming Conference, Uppsala, 1984, 263\u2013276."},{"key":"17_CR16","first-page":"679","volume-title":"Lecture Notes in Artificial Intelligence 449","author":"D.A. Wolfram","year":"1990","unstructured":"D.A. Wolfram, ACE: the abstract clause engine, System Summary, Proceedings of the Tenth International Conference on Automated Deduction, Kaiserslautern, Federal Republic of Germany, 23\u201327 July 1990, Lecture Notes in Artificial Intelligence 449, Springer, Berlin, 1990, 679\u2013680."},{"key":"17_CR17","doi-asserted-by":"crossref","unstructured":"D.A. Wolfram, The Clausal Theory of Types, Cambridge Tracts in Theoretical Computer Science 21, Cambridge, 1993.","DOI":"10.1017\/CBO9780511569906"}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58085-9_85.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:16:53Z","timestamp":1605647813000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58085-9_85"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540580850","9783540484400"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-58085-9_85","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}