{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T16:31:59Z","timestamp":1725467519191},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540649878"},{"type":"electronic","value":"9783540498018"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0055141","type":"book-chapter","created":{"date-parts":[[2006,7,27]],"date-time":"2006-07-27T05:09:13Z","timestamp":1153976953000},"page":"263-276","source":"Crossref","is-referenced-by-count":0,"title":["Free variables and subexpressions in higher-order meta logic"],"prefix":"10.1007","author":[{"given":"Chuck","family":"Liang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,5,27]]},"reference":[{"issue":"2\/3","key":"16_CR1","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"1988","unstructured":"Thierry Coquand and G\u00e9rard Huet. The calculus of constructions. Information and Computation, 76(2\/3):95\u2013120, February\/March 1988.","journal-title":"Information and Computation"},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"Jo\u00cblle Despeyroux, Amy Felty, and Andr\u00e9 Hirschowitz. Higher-order abstract syntax in Coq. In Second International Conference on Typed Lambda Calculi and Applications, pages 124\u2013138. Springer-Verlag Lecture Notes in Computer Science, April 1995.","DOI":"10.1007\/BFb0014049"},{"key":"16_CR3","doi-asserted-by":"crossref","unstructured":"Amy Felty. A logic programming approach to implementing higher-order term rewriting. In Lars-Henrik Eriksson, Lars Halln\u00c4s, and Peter Schroeder-Heister, editors, Proceedings of the January 1991 Workshop on Extensions to Logic Programming, volume 596 of Lecture Notes in Artificial Intelligence, pages 135\u2013161. Springer-Verlag, 1992.","DOI":"10.1007\/BFb0013606"},{"issue":"1","key":"16_CR4","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/BF00881900","volume":"11","author":"A. Felty","year":"1993","unstructured":"Amy Felty. Implementing tactics and tacticals in a higher-order logic programming language. Journal of Automated Reasoning, 11(1):43\u201381, August 1993.","journal-title":"Journal of Automated Reasoning"},{"issue":"2","key":"16_CR5","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1017\/S0956796800000666","volume":"3","author":"J. Hannan","year":"1993","unstructured":"John Hannan. Extended natural semantics. Journal of Functional Programming, 3(2):123\u2013152, April 1993.","journal-title":"Journal of Functional Programming"},{"key":"16_CR6","unstructured":"P. M. Hill and J. G. Gallagher. Meta-programming in logic programming. Technical Report Report 94.22, University of Leeds, hill@scs.leeds.ac.uk, August 1994. To appear in Vol. 5 of the Handbook of Logic in Artificial Intelligence and Logic Programming, Oxford University Press."},{"key":"16_CR7","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"G. Huet","year":"1975","unstructured":"G\u00e9rard Huet. A unification algorithm for typed \u03bb-calculus. Theoretical Computer Science, 1:27\u201357, 1975.","journal-title":"Theoretical Computer Science"},{"key":"16_CR8","unstructured":"Chuck Liang. Substitution, Unification and Generalization in Meta-Logic. PhD thesis, University of Pennsylvania, September 1995."},{"key":"16_CR9","first-page":"490","volume":"1214","author":"C. Liang","year":"1997","unstructured":"Chuck Liang. Let-polymorphism and eager type schemes. In TAPSOFT '97: Theory and Practice of Software Development, pages 490\u2013501. Springer Verlag LNCS Vol. 1214, 1997.","journal-title":"Springer Verlag LNCS"},{"key":"16_CR10","doi-asserted-by":"crossref","unstructured":"R. McDowell and D. Miller. A logic for reasoning with higher-order abstract syntax. In Symposium on Logic in Computer Science. IEEE, 1997.","DOI":"10.1109\/LICS.1997.614968"},{"key":"16_CR11","unstructured":"Dale Miller. Abstractions in logic programming. In Piergiorgio Odifreddi, editor, Logic and Computer Science, pages 329\u2013359. Academic Press, 1990."},{"issue":"4","key":"16_CR12","doi-asserted-by":"crossref","first-page":"497","DOI":"10.1093\/logcom\/1.4.497","volume":"1","author":"D. Miller","year":"1991","unstructured":"Dale Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. Journal of Logic and Computation, 1(4):497\u2013536, 1991.","journal-title":"Journal of Logic and Computation"},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"Dale Miller. Unification under a mixed prefix. Journal of Symbolic Computation, pages 321\u2013358, 1992.","DOI":"10.1016\/0747-7171(92)90011-R"},{"key":"16_CR14","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/0168-0072(91)90068-W","volume":"51","author":"D. Miller","year":"1991","unstructured":"Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic, 51:125\u2013157, 1991.","journal-title":"Annals of Pure and Applied Logic"},{"key":"16_CR15","doi-asserted-by":"crossref","unstructured":"Tobias Nipkow. Higher-order critical pairs. In G. Kahn, editor, Sixth Annual Symposium on Logic in Computer Science, pages 342\u2013349. IEEE, July 1991.","DOI":"10.1109\/LICS.1991.151658"},{"key":"16_CR16","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/BF00248324","volume":"5","author":"L. C. Paulson","year":"1989","unstructured":"Lawrence C. Paulson. The foundation of a generic theorem prover. Journal of Automated Reasoning, 5:363\u2013397, September 1989.","journal-title":"Journal of Automated Reasoning"},{"key":"16_CR17","doi-asserted-by":"crossref","unstructured":"Frank Pfenning and Conal Elliot. Higher-order abstract syntax. In Proceedings of the ACM-SIGPLAN Conference on Programming Language Design and Implementation, pages 199\u2013208. ACM Press, June 1988.","DOI":"10.1145\/53990.54010"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0055141","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,20]],"date-time":"2019-04-20T04:34:35Z","timestamp":1555734875000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0055141"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540649878","9783540498018"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/bfb0055141","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}