{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:18:32Z","timestamp":1725664712416},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540613770"},{"type":"electronic","value":"9783540685074"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61377-3_34","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T16:36:07Z","timestamp":1330274167000},"page":"106-129","source":"Crossref","is-referenced-by-count":2,"title":["Representing unification in a logical framework"],"prefix":"10.1007","author":[{"given":"Jason","family":"Brown","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lincoln A.","family":"Wallen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"7_CR1","unstructured":"H. P. Barendregt. The Lambda Calculus, its syntax and semantics. North Holland, 1984."},{"key":"7_CR2","unstructured":"R. Boyer and J. Moore. A Computational Logic. Academic Pres, 1979."},{"key":"7_CR3","unstructured":"Jason Brown and Eike Ritter. \u03bb\u03c0-calculus with type similarity. Technical Report PRG-TR-1-95, Oxford University Computing Laboratory, January 1995."},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"Jason Brown. Presentations of Unification in a Logical Framework. DPhil thesis, University of Oxford, submitted January 1996.","DOI":"10.1007\/3-540-61377-3_34"},{"key":"7_CR5","first-page":"29","volume-title":"The mathematical language AUTOMATH, its usage, and some of its extensions","author":"N. G. Bruijn de","year":"1968","unstructured":"N. G. de Bruijn. The mathematical language AUTOMATH, its usage, and some of its extensions. In M. Laudet, editor, Proceedings of the Symposium on Automatic Demonstration, pages 29\u201361, Versailles, France, December 1968. Springer-Verlag LNM 125."},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"N. G. de Bruijn. A plea for weaker frameworks. In G. Huet and G. Plotkin, editors, Logical Frameworks, pages 149\u2013181. Cambridge University Press, 1991.","DOI":"10.1017\/CBO9780511569807.004"},{"key":"7_CR7","volume-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"R. L. Constable","year":"1986","unstructured":"R. L. Constable, et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Englewood Cliffs, New Jersey, 1986."},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"Conal Elliott. Higher-order unification with dependent type functions. In N. Dershowitz, editor, Proceedings of the 3rd International Conference on Rewriting Techniques and Applications, volume 355 of LNCS, pages 121\u2013136. Springer-Verlag, 1989.","DOI":"10.1007\/3-540-51081-8_104"},{"key":"7_CR9","unstructured":"Conal Elliott. Extensions and Applications of Higher-Order Unification. PhD thesis, School of Computer Science, Carnegie Mellon University, 1990."},{"key":"7_CR10","unstructured":"Herman Geuvers. Logics and Type Systems. PhD thesis, Katholieke Universiteit Nijmegen, 1993."},{"key":"7_CR11","doi-asserted-by":"crossref","unstructured":"M. Gordon, R, Milner and C. Wadsworth. Edinburgh LCF: A Mechanized Logic of Computation. In volume 78 of LNCS. Springer-Verlag, 1979.","DOI":"10.1007\/3-540-09724-4"},{"issue":"1","key":"7_CR12","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1993","unstructured":"Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the ACM, 40(1):143\u2013184, January 1993.","journal-title":"Journal of the ACM"},{"key":"7_CR13","doi-asserted-by":"crossref","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"},{"volume-title":"Logical Frameworks","year":"1991","key":"7_CR14","unstructured":"G\u00e9rard Huet and Gordon Plotkin, editors. Logical Frameworks. Cambridge University Press, Cambridge, 1991."},{"volume-title":"Logical Environments","year":"1993","key":"7_CR15","unstructured":"Gerard Huet and Gordon Plotkin, editors. Logical Environments. Cambridge University Press, Cambridge, 1993."},{"issue":"1","key":"7_CR16","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1016\/0304-3975(76)90021-9","volume":"3","author":"D. Jensen","year":"1976","unstructured":"D. Jensen and T. Pietrzykowski. Mechanizing w-order type theory through unification. Theoretical Computer Science, 3(1):123\u2013171, 1976.","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"7_CR17","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1007\/BF00244282","volume":"8","author":"R. Letz","year":"1992","unstructured":"R. Letz, J. Schumann, S. Boyerl and W. Bibel. SETHEO: a high-performance theorem prover. Journal of Automated Reasoning, 8(2):183\u2013212, 1992.","journal-title":"Journal of Automated Reasoning"},{"issue":"2","key":"7_CR18","doi-asserted-by":"crossref","first-page":"258","DOI":"10.1145\/357162.357169","volume":"4","author":"A. Martelli","year":"1982","unstructured":"Alberto Martelli and Ugo Montanari. An efficient unification algorithm. ACM Transactions on Programming Languages and Systems, 4(2):258\u2013282, 1982.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"7_CR19","unstructured":"L. Paulson. Isabelle: The next 700 theorem provers. In P. Odifreddi, editor, Logic and Computer Science, pages 361\u2013386. Academic Press, 1990."},{"key":"7_CR20","doi-asserted-by":"crossref","unstructured":"Frank Pfenning. Logic Programming in the LF logical framework. In G. Huet and G. Plotkin, editors, Logical Frameworks, pages 149\u2013181. Cambridge University Press, 1991.","DOI":"10.1017\/CBO9780511569807.008"},{"key":"7_CR21","unstructured":"David Pym. Proofs, Search and Computation in General Logic. PhD thesis, Laboratory for the Foundations of Computer Science University of Edinburgh, 1990. Available as technical report no. CST-69-90."},{"issue":"3","key":"7_CR22","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1142\/S012905419200019X","volume":"3","author":"D. Pym","year":"1992","unstructured":"David Pym. A unification algorithm for the \u03bb\u03c0-Calculus. International Journal of Foundations of Computer Science, 3(3):333\u2013378, 1992.","journal-title":"International Journal of Foundations of Computer Science"},{"key":"7_CR23","doi-asserted-by":"crossref","unstructured":"David Pym and Lincoln Wallen. Proof search in the \u03bb\u03c0-calculus. In G. Huet and G. Plotkin, editors, Logical Frameworks, pages 309\u2013340. Cambridge University Press, 1991.","DOI":"10.1017\/CBO9780511569807"},{"key":"7_CR24","unstructured":"A. Salvesen. The Church-Rosser property for \u03b2\u03b7-reduction. Manuscript, 1991. p"},{"key":"7_CR25","doi-asserted-by":"crossref","unstructured":"Wayne Snyder. A proof theory for general unification. Birkhauser, 1991.","DOI":"10.1007\/978-1-4612-0435-0"},{"key":"7_CR26","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1016\/S0747-7171(89)80023-9","volume":"8","author":"W. Snyder","year":"1989","unstructured":"Wayne Snyder and Jean Gallier. Higher-order unification revisited: Complete sets of transformations. Journal of Symbolic Computation, 8:101\u2013140, 1989.","journal-title":"Journal of Symbolic Computation"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61377-3_34.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,31]],"date-time":"2021-12-31T05:34:23Z","timestamp":1640928863000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61377-3_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540613770","9783540685074"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/3-540-61377-3_34","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}