{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,12]],"date-time":"2025-06-12T10:43:52Z","timestamp":1749725032769},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540617808"},{"type":"electronic","value":"9783540707226"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61780-9_70","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:25:22Z","timestamp":1330277122000},"page":"183-200","source":"Crossref","is-referenced-by-count":2,"title":["An algorithm for checking incomplete proof objects in type theory with localization and unification"],"prefix":"10.1007","author":[{"given":"Lena","family":"Magnusson","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"issue":"2","key":"13_CR1","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1017\/S0956796800020025","volume":"1","author":"H. P. Barendregt","year":"1991","unstructured":"H. P. Barendregt. Introduction to Generalized Type Systems. J. Functional Programming, 1(2):125\u2013154, April 1991.","journal-title":"J. Functional Programming"},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"Thierry Coquand. An algorithm for testing conversion in type theory. In Logical Frameworks. Cambridge University Press, 1991.","DOI":"10.1017\/CBO9780511569807.011"},{"issue":"3","key":"13_CR3","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1093\/logcom\/3.3.287","volume":"3","author":"G. Dowek","year":"1993","unstructured":"Gilles Dowek. A Complete Proof Synthesis Method for the Cube of Type Systems. Journal of Logic and Computation, 3(3):287\u2013315, 1993.","journal-title":"Journal of Logic and Computation"},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"Conal M. Elliot. Higher-order unification with dependent function types. In N. Dershowitz, editor, Proceedings of the 3rd International Conference on Rewriting Techniques and Applications, pages 121\u2013136, April 1989.","DOI":"10.1007\/3-540-51081-8_104"},{"key":"13_CR5","first-page":"479","volume-title":"To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"W. A. Howard","year":"1980","unstructured":"W. A. Howard. The formulae-as-types notion of construction. In J. P. Seldin and J. R. Hindley, editors, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 479\u2013490. Academic Press, London, 1980."},{"issue":"1","key":"13_CR6","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(1):27\u201357, 1975.","journal-title":"Theoretical Computer Science"},{"key":"13_CR7","unstructured":"Lena Magnusson. The Implementation of ALF \u2014 a Proof Editor based on Martin-L\u00f6f's Monomorphic Type Theory with Explicit Substitution. PhD thesis, G\u00f6teborg University and Chalmers University of Technology, January 1995."},{"key":"13_CR8","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/3-540-58085-9_78","volume-title":"Types for Proofs and Programs","author":"L. Magnusson","year":"1994","unstructured":"Lena Magnusson and Bengt Nordstr\u00f6m. The ALF proof editor and its proof engine. In Types for Proofs and Programs, LNCS, pages 213\u2013237, Nijmegen, 1994. Springer-Verlag."},{"key":"13_CR9","doi-asserted-by":"crossref","unstructured":"James McKinna and Randy Pollack. Pure type system formalized. In M. Bezem and J.F. Groote, editors, Proceeding of the International Conference on Typed Lambda Calculi and Applications, TLCA '93, pages 289\u2013305. Springer-Verlag, LNCS 664, March 1993.","DOI":"10.1007\/BFb0037113"},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"Randy Pollack. Closure under Alpha conversion. In The Informal Proceeding of the 1993 Workshop on Types for Proofs and Programs, May 1993.","DOI":"10.1007\/3-540-58085-9_82"},{"key":"13_CR11","unstructured":"David Pym. A unification algorithm for the logical framework. Technical Report ECS-LFCS-92-229, University of Edinburgh, August 1992."},{"key":"13_CR12","volume-title":"Technical report","author":"A. Salvesen","year":"1988","unstructured":"Anne Salvesen. Polymorphism and Monomorphism in Martin-L\u00f6f's Type Theory. Technical report, Norwegian Computing Center, P.b. 114, Blindern, 0316 Oslo 3, Norway, December 1988."},{"key":"13_CR13","volume-title":"Licentiate Thesis","author":"A. Tasistro","year":"1993","unstructured":"Alvaro Tasistro. Formulation of Martin-L\u00f6f's Theory of Types with Explicit Substitution. Licentiate Thesis, Chalmers University of Technology and University of G\u00f6teborg, Sweden, May 1993."},{"key":"13_CR14","volume-title":"Technical Report 1684","author":"L. Th\u00e9ry","year":"1992","unstructured":"L. Th\u00e9ry, Y. Bertot, and G. Kahn. Real Theorem Provers Deserve Real User-Interfaces. Technical Report 1684, INRIA Sophia-Antipolis, May 1992."}],"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-61780-9_70.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:10:56Z","timestamp":1605629456000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61780-9_70"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540617808","9783540707226"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-61780-9_70","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}