{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:30:37Z","timestamp":1774837837764,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540617808","type":"print"},{"value":"9783540707226","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61780-9_59","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T22:25:33Z","timestamp":1330295133000},"page":"16-35","source":"Crossref","is-referenced-by-count":14,"title":["A two-level approach towards lean proof-checking"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[]},{"given":"Mark","family":"Ruys","sequence":"additional","affiliation":[]},{"given":"Henk","family":"Barendregt","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"2_CR1","unstructured":"A. Bailey. Representing algebra in Lego, M.Sc. thesis, University of Edinburgh, October 1993."},{"key":"2_CR2","unstructured":"C. Ballarins, K. Homann and J. Calmet. Theorems and algorithms: an interface between Maple and Isabelle, in the proceedings of ISSAC'95."},{"key":"2_CR3","unstructured":"H.P. Barendregt. Typed \u03bb-calculi, Handbook of logic in computer science, Abramsky and al eds, OUP 1992."},{"key":"2_CR4","unstructured":"G. Barthe. Towards a mathematical vernacular, manuscript, presented at the HISC workshop, Amsterdam, March 1994."},{"key":"2_CR5","unstructured":"G. Barthe. Formalising mathematics in type theory: fundamentals and case studies, manuscript, June 1994, submitted for publication."},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"G. Barthe and H. Elbers. Towards lean proof checking, to appear in the proceedings of DISCO'96, Lecture Notes in Computer Science, Springer-Verlag, 1996. An extended version will appear as a CWI technical report.","DOI":"10.1007\/3-540-61697-7_5"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"G. Barthe and H. Geuvers. Congruence types, to appear in the proceedings of CSL'95, 1995.","DOI":"10.1007\/3-540-61377-3_30"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"G. Barthe, M. Ruys and H. Barendregt. A two-level approach towards lean proofchecking, to appear as a CWI technical report, 1996.","DOI":"10.1007\/3-540-61780-9_59"},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"V. Breazu-Tannen. Combining algebra and higher-order types, in the proceedings of LICS'88, pp 82\u201390, IEEE, 1988.","DOI":"10.1109\/LICS.1988.5103"},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"P. Cohn. Universal algebra, Mathematics and its Applications, Vol. 6, D. Reidel, 1981.","DOI":"10.1007\/978-94-009-8399-1"},{"key":"2_CR11","unstructured":"R. Constable. Metalevel Programming in Constructive Type Theory, Logic and Algebra of Specification, F. Bauer and al eds, NATO Asi Series, 1994."},{"key":"2_CR12","unstructured":"R. Constable and al. Implementing mathematics with the NuPrl proof development system, Prentice Hall, 1986."},{"key":"2_CR13","unstructured":"G. Dowek and al. The Coq proof assistant user's guide Technical Report, INRIA, November 1993."},{"key":"2_CR14","unstructured":"H. Elbers. A machine-assisted construction of the real numbers, M.Sc. thesis, University of Nijmegen, September 1993."},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"J. Harrison and L. Th\u00e9ry. Extending the HOL theorem prover with a computer algebra system to reason about the reals, in proceedings of HOL'93, LNCS, 1993.","DOI":"10.1007\/3-540-57826-9_134"},{"key":"2_CR16","unstructured":"D. Howe. Automating reasoning in an implementation of constructive type theory, Ph.D. thesis, Cornell University, 1988."},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"P. Jackson. Exploring abstract algebra in constructive type theory, in the proceedings of CADE-12, LNAI 814, June 1994.","DOI":"10.1007\/3-540-58156-1_43"},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"J.W. Klop. Term-rewriting systems, in Handbook of logic in computer science (volume 2), Abramsky and al eds, OUP 1992.","DOI":"10.1093\/oso\/9780198537618.003.0001"},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"Z. Luo. Computation and reasoning: a type theory for computer science, OUP, 1994.","DOI":"10.1093\/oso\/9780198538356.001.0001"},{"key":"2_CR20","unstructured":"Z. Luo and R. Pollack. LEGO proof development system: user's manual, Technical Report, University of Edinburgh, May 1992."},{"key":"2_CR21","doi-asserted-by":"crossref","unstructured":"L. Magnusson and B. Nordstr\u00f6m. The Alf proof editor and its proof engine, in the proceedings of Types for Proofs and Programs, LNCS 806, May 1993.","DOI":"10.1007\/3-540-58085-9_78"},{"key":"2_CR22","unstructured":"P. Martin-L\u00f6f. An intuitionistic theory of types, Bibliopolis, 1984."},{"key":"2_CR23","unstructured":"R. Nederpelt and al. Selected papers on AUTOMATH, North-Holland, 1994."},{"key":"2_CR24","unstructured":"B. Nordstr\u00f6m, K. Petersson and J. Smith. Programming in Martin-L\u00f6f 's type theory, OUP, 1990."},{"key":"2_CR25","unstructured":"M.P.J. Ruys. Ph.D. thesis, University of Nijmegen, forthcoming (1996)."}],"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_59.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T23:26:37Z","timestamp":1742599597000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61780-9_59"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540617808","9783540707226"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/3-540-61780-9_59","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996]]}}}