{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T23:11:11Z","timestamp":1784848271554,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540651376","type":"print"},{"value":"9783540495628","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0097785","type":"book-chapter","created":{"date-parts":[[2006,11,24]],"date-time":"2006-11-24T09:27:48Z","timestamp":1164360468000},"page":"28-45","source":"Crossref","is-referenced-by-count":6,"title":["Verification of the interface of a small proof system in coq"],"prefix":"10.1007","author":[{"given":"Bruno","family":"Barras","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2006,10,26]]},"reference":[{"key":"3_CR1","unstructured":"Barendregt, H.: Lambda Calculi with Types. In Handbook of Logic in Computer Science, Vol II, Elsevier, 1992."},{"key":"3_CR2","unstructured":"Barras, B.: Coq en Coq. Rapport de Recherche INRIA 3026. Octobre 1996."},{"key":"3_CR3","unstructured":"Barras, B., Werner, B.: Coq in Coq. Submitted to publication. http:\/\/pauillac.inria.fr\/~barras\/coqincoq.ps.gz"},{"key":"3_CR4","unstructured":"Barras, B., Boutin, S., Cornes, C., Courant, J., Filli\u00e2tre, J.-C., Gim\u00e9nez, E., Herbelin, H., Huet, G., Mu\u00f1oz, C., Murthy, C., Parent, C., Paulin-Mohring, C., Sa\u00efbi, A., Werner, B.: The Coq Proof Assistant Reference Manual Version 6.1. Technical Report 0203. Coq Project-INRIA Rocquencourt-ENS Lyon. May 97."},{"key":"3_CR5","unstructured":"Boyer, R.S., Dowek, G.: Towards Checking Proof-Checkers. In Herman Geuvers, editor, Informal Proceedings of the Nijmegen Workshop on Types for Proofs and Programs, May 1993."},{"issue":"5","key":"3_CR6","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":"De Bruijn, N.J.: Lambda-Calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem. Indag. Math. Vol. 34 (5), pp 381\u2013392, 1972.","journal-title":"Indag. Math."},{"key":"3_CR7","first-page":"95","volume-title":"Information and Computation","author":"T. Coquand","year":"1988","unstructured":"Coquand, T., Huet, G.: The Calculus of Constructions. In: Information and Computation Vol. 76, February\/March 1988 (ed. A.R. Meyer), Academic Press, London, 95\u2013120."},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Coscoy, Y., Khan, G., Th\u00e9ry, L.: Extracting text from proofs. INRIA Research Report 2459. January 1995.","DOI":"10.1007\/BFb0014048"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Courant, J.: A Module Calculus for Pure Type Systems. In: Proceedings of the Third International Conference on Typed Lambda Calculi and Applications, TLCA'97, Nancy (ed. Ph. de Groote and J. R. Hindley), Springer-Verlag, LNCS 1210, April 1997.","DOI":"10.1007\/3-540-62688-3_32"},{"key":"3_CR10","unstructured":"Girard, J.-Y., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge Tracts in Theoretical Computer Science 7. Cambridge University Press."},{"issue":"2","key":"3_CR11","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1017\/S0956796800020037","volume":"1","author":"H. Geuvers","year":"1991","unstructured":"Geuvers, H., Nederhof, M.-J.: A Modular Proof of Strong Normalization for the Calculus of Constructions. Journal of Functional Programming, 1(2):155\u2013189, April 1991.","journal-title":"Journal of Functional Programming"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Gordon, M., Milner, R., Wadsworth, C.: Edinburgh LCF: A Mechanized Logic of Computation. Springer-Verlag, LNCS 78, 1979.","DOI":"10.1007\/3-540-09724-4"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Huet, G.: The Constructive Engine. In R. Narasimhan, editor, A Perspective in Theoretical Computer Science. WorldScientific Publishing, 1989. Commemorative Volume for Gift Siromoney.","DOI":"10.1142\/9789814368452_0004"},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"Leroy, X.: Applicative Functors and Fully Transparent Higher-Order Modules. In: 22nd Symposium on Principles of Programming Languages, pp. 142\u2013153. ACM Press, 1995.","DOI":"10.1145\/199448.199476"},{"key":"3_CR15","unstructured":"Martin-L\u00f6f, P.: A Theory of Types. Technical Report 71-3, University of Stockholm, 1971."},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"Paulin-Mohring, C., Werner, B.: Synthesis of ML programs in Coq. Journal of Symbolic Computation-special issue on automated programming, 1993.","DOI":"10.1016\/S0747-7171(06)80007-6"},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"Pollack, R.: Closure Under Alpha-Conversion. In: Types for Proofs and Programs: International Workshop TYPES'93, Nijmegen, May 1993, Selected Papers, file:\/\/ftp.dcs.ed.ac.uk\/pub\/lego\/alpha-closure.ps.gz (ed. H. Barendregt and T. Nipkow), Springer-Verlag, pp. 313\u2013332, LNCS 806, 1994.","DOI":"10.1007\/3-540-58085-9_82"},{"key":"3_CR18","unstructured":"Pollack, R.: A Proof Checker for the Extended Calculus of Constructions. Ph. D. Thesis, ftp:\/\/ftp.dcs.ed.ac.uk\/pub\/lego\/thesis-pollack.ps.Z University of Edinburgh, 1994."},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"Pollack, R.: A Verified Typechecker. In: Proceedings of the Second International Conference on Typed Lambda Calculi and Applications, TLCA'95, Edinburgh, (ed. M. Dezani-Ciancaglini and G. Plotkin), Springer-Verlag, LNCS 902, April 1995.","DOI":"10.1007\/BFb0014065"}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0097785","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,18]],"date-time":"2020-04-18T23:20:32Z","timestamp":1587252032000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0097785"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540651376","9783540495628"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/bfb0097785","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1998]]}}}