{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:30:39Z","timestamp":1761597039926},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540678632"},{"type":"electronic","value":"9783540446590"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44659-1_2","type":"book-chapter","created":{"date-parts":[[2007,7,21]],"date-time":"2007-07-21T13:40:26Z","timestamp":1185025226000},"page":"17-37","source":"Crossref","is-referenced-by-count":20,"title":["Programming and Computing in HOL"],"prefix":"10.1007","author":[{"given":"Bruno","family":"Barras","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. L\u00e9vy. Explicit substitutions. In Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, San Francisco, California, pages 31\u201346. ACM, January 1990. Also Digital Equipment Corporation, Systems Research Center, Research Report 54, February 1990.","DOI":"10.1145\/96709.96712"},{"key":"2_CR2","unstructured":"H. Barendregt. Lambda Calculi with Types. Technical Report 91-19, Catholic University Nijmegen, 1991. In Handbook of Logic in Computer Science, Vol II."},{"key":"2_CR3","unstructured":"B. Barras. Auto-validation d\u2019un syst\u00e8me de preuves avec familles inductives. Th\u00e8se de doctorat, Universit\u00e9 Paris 7, November 1999."},{"key":"2_CR4","unstructured":"B. Barras, S. Boutin, C. Cornes, J. Courant, J.-C. Filli\u00e2tre, E. Gim\u00e9nez, H. Herbelin, G. Huet, C. Mu\u00f1oz, C. Murthy, C. Parent, C. Paulin, A. Sa\u00efbi, and B. Werner. The Coq Proof Assistant Reference Manual version 6.1. Technical Report 0203, Projet Coq-INRIA Rocquencourt-ENS Lyon, August 1997."},{"issue":"1\/2","key":"2_CR5","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/BF01383983","volume":"3","author":"R.J. Boulton","year":"1993","unstructured":"R.J. Boulton. Lazy techniques for fully expansive theorem proving. Formal Methods in System Design, 3(1\/2):25\u201347, August 1993.","journal-title":"Formal Methods in System Design"},{"key":"2_CR6","series-title":"Lect Notes Comput Sci","volume-title":"TACS\u201997","author":"S. Boutin","year":"1997","unstructured":"S. Boutin. Using reflection to build efficient and certified decision procedures. In Martin Abadi and Takahashi Ito, editors, TACS\u201997, volume 1281. LNCS, Springer-Verlag, 1997."},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"P. Cr\u00e9gut. An abstract machine for \u03bb-terms normalization. In Gilles Kahn, editor, Proceedings of the ACM Conference on LISP and Functional Programming, pages 333\u2013340, Nice, France, June 1990. ACM Press.","DOI":"10.1145\/91556.91681"},{"issue":"2","key":"2_CR8","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1145\/226643.226675","volume":"43","author":"P.-L. Curien","year":"1996","unstructured":"Pierre-Louis Curien, Th\u00e9r\u00e8se Hardin, and Jean-Jacques Levy. Confluence properties of weak and strong calculi of explicit substitutions. Journal of the ACM, 43(2):362\u2013397, March 1996.","journal-title":"Journal of the ACM"},{"issue":"5","key":"2_CR9","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"N.J. Bruijn De","year":"1972","unstructured":"N.J. De Bruijn. Lambda-calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem. Indag. Math., 34(5), pp. 381\u2013392, 1972.","journal-title":"Indag. Math."},{"key":"2_CR10","unstructured":"M. J. C. Gordon and T. F. Melham. Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, 1993."},{"key":"2_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF","author":"M. J. Gordon","year":"1979","unstructured":"M. J. Gordon, R. Milner, and C. Wadsworth. Edinburgh LCF. LNCS 78. Springer-Verlag, 1979."},{"key":"2_CR12","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of the International Conference on Typed Lambda Calculi and Applications","author":"P.-A. Melli\u00e8s","year":"1995","unstructured":"P.-A. Melli\u00e8s. Typed \u03bb-calculi with explicit substitutions may not terminate. In M. Dezani-Ciancaglini and G. Plotkin, editors, Proceedings of the International Conference on Typed Lambda Calculi and Applications, Edinburgh, Scotland, April 1995. Springer-Verlag LNCS 902."},{"key":"2_CR13","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/0167-6423(83)90008-4","volume":"3","author":"L. C. Paulson","year":"1983","unstructured":"Lawrence C. Paulson. A higher-order implementation of rewriting. Science of Computer Programming, 3:119\u2013149, 1983.","journal-title":"Science of Computer Programming"},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"Lawrence C. Paulson. Logic and Computation: Interactive proof with Cambridge LCF. Cambridge University Press, 1987.","DOI":"10.1017\/CBO9780511526602"},{"key":"2_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1007\/BFb0105417","volume-title":"Theorem Proving in Higher Order Logics: 9th International Conference, Turku, Finland","author":"K. Slind","year":"1996","unstructured":"K. Slind. Function definition in higher order logic. In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem Proving in Higher Order Logics: 9th International Conference, Turku, Finland, volume 1125, pages 381\u2013397. LNCS, Springer-Verlag, August 1996."}],"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\/3-540-44659-1_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T07:33:03Z","timestamp":1556695983000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44659-1_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540678632","9783540446590"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-44659-1_2","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}