{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:28:19Z","timestamp":1761611299834},"publisher-location":"Berlin, Heidelberg","reference-count":24,"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_78","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T15:11:03Z","timestamp":1330269063000},"page":"213-237","source":"Crossref","is-referenced-by-count":55,"title":["The Alf proof editor and its proof engine"],"prefix":"10.1007","author":[{"given":"Lena","family":"Magnusson","sequence":"first","affiliation":[]},{"given":"Bengt","family":"Nordstr\u00f6m","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"10_CR1","volume-title":"Licentiate Thesis","author":"G. Betarte","year":"1993","unstructured":"Gustavo Betarte. A case study in machine-assisted proofs: The integers form an integral domain. Licentiate Thesis, Chalmers University of Technology and University of G\u00f6teborg, Sweden, November 1993."},{"key":"10_CR2","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, NJ, 1986."},{"key":"10_CR3","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"},{"key":"10_CR4","unstructured":"Thierry Coquand. Pattern matching with dependent types. In Proceeding from the logical framework workshop at B\u00e5stad, June 1992."},{"key":"10_CR5","unstructured":"Thierry Coquand and G\u00e9rard Huet. The Calculus of Constructions. Technical Report 530, INRIA, Centre de Rocquencourt, 1986."},{"key":"10_CR6","unstructured":"N.G. de Bruijn. Generalizing automath by means of a lambda-typed lambda calculus. In Mathematical Logic and Theoretical Computer Science, Lecture Notes in pure and applied mathematics, pages 71\u201392. 1987."},{"key":"10_CR7","unstructured":"G. Dowek, A. Felty, H. Herbelin, H. Huet, G. P. Murthy, C. Parent, C. Paulin-Mohring, and B. Werner. The coq proof assistant user's guide version 5.6. Technical report, Rapport Technique 134, INRIA, December 1991."},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Conal M. Elliot. Higher-order unification with dependent function types. In N. Derikowitz, 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":"10_CR9","unstructured":"Veronica Gaspes. Formal Proofs of Combinatorial Completeness. In To appear in the informal proceedings from the logical framework workshop at B\u00e5stad, June 1992."},{"key":"10_CR10","unstructured":"Gerhard Gentzen. Investigations into Logical Deduction. In E. Szabo, editor, The Collected Papers of Gerhard Gentzen. North-Holland Publishing Company, 1969."},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"M. Gordon, R. Milner, and C. Wadsworth. Edinburgh LCF, volume 78 of Lecture Notes in Computer Science. Springer-Verlag, 1979.","DOI":"10.1007\/3-540-09724-4"},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"Martin Hofmann. A model of intensional martin-l\u00f6f type theory in which unicity of identity proofs does not hold. Technical report, Dept. of Computer Science, University of Edinburgh, June 1993. Draft.","DOI":"10.1007\/3-540-58085-9_76"},{"issue":"1","key":"10_CR13","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(1):27\u201357, 1975.","journal-title":"Theoretical Computer Science"},{"key":"10_CR14","unstructured":"G. Kahn. L. Thery, Y. Bertot. Real Theorem Provers Deserve Real User-Interfaces. Technical report, INRIA, Rocquencourt, 1992."},{"key":"10_CR15","unstructured":"Z. Luo and R. Pollack. LEGO Proof Development System: User's Manual. Technical report, LFCS Technical Report ECS-LFCS-92-211, 1992."},{"key":"10_CR16","unstructured":"Lena Magnusson. Refinement and local undo in the interactive proof editor ALF. In The Informal Proceeding of the 1993 Workshop on Types for Proofs and Programs, May 1993."},{"key":"10_CR17","unstructured":"Bengt Nordstr\u00f6m, Kent Petersson, and Jan M. Smith. Programming in Martin-L\u00f6f's Type Theory. An Introduction. Oxford University Press, 1990."},{"key":"10_CR18","volume-title":"Technical report 189","author":"L. C. Paulson","year":"1990","unstructured":"Lawrence C. Paulson and Tobias Nipkow. Isabelle tutorial and user's manual. Technical report 189, Universtiy of Cambridge Computer Laboratory, Cambridge, January 1990."},{"key":"10_CR19","volume-title":"PMG report 9","author":"K. Petersson","year":"1982","unstructured":"Kent Petersson. A Programming System for Type Theory. PMG report 9, Chalmers University of Technology, S-412 96 G\u00f6teborg, 1982, 1984."},{"key":"10_CR20","unstructured":"David Pym. A unification algorithm for the logical framework: Technical Report ECS-LFCS-92-229, University of Edinburgh, August 1992."},{"key":"10_CR21","volume-title":"Technical report","author":"A. Salvesen","year":"1988","unstructured":"Anne Salvesen. Polymorphism and Monomorphism in Martin-L\u00f6fs Type Theory. Technical report, Norwegian Computing Center, P.b. 114, Blindem, 0316 Oslo 3, Norway, December 1988."},{"key":"10_CR22","unstructured":"Nora Szasz. A Machine Checked Proof that Ackermann's Function is not Primitive Recursive. Licentiate Thesis, Chalmers University of Technology and University of G\u00f6teborg, Sweden, June 1991. To appear in G. Huet and G. Plotkin, editors, Logical Frameworks, Cambridge University Press."},{"key":"10_CR23","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":"10_CR24","unstructured":"Bj\u00f6rn von Sydow. A machine-assisted proof of the fundamental theorem of arithmetic. Pmg memo, Chalmers University of Technology, 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-58085-9_78.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:16:50Z","timestamp":1605647810000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58085-9_78"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540580850","9783540484400"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-58085-9_78","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}