{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,6]],"date-time":"2025-06-06T04:06:54Z","timestamp":1749182814694,"version":"3.41.0"},"reference-count":20,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[2002,9,1]],"date-time":"2002-09-01T00:00:00Z","timestamp":1030838400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2002,9,1]],"date-time":"2002-09-01T00:00:00Z","timestamp":1030838400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Automated Reasoning"],"published-print":{"date-parts":[[2002,9]]},"DOI":"10.1023\/a:1021923116629","type":"journal-article","created":{"date-parts":[[2003,3,21]],"date-time":"2003-03-21T23:56:29Z","timestamp":1048290989000},"page":"277-307","source":"Crossref","is-referenced-by-count":7,"title":["Proof Reflection in Coq"],"prefix":"10.1007","volume":"29","author":[{"given":"Dimitri","family":"Hendriks","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5109768_CR1","unstructured":"Altenkirch, T.: Constructions, inductive types and strong normalisation, Ph.D. thesis, Laboratory for the Foundations of Computer Science, University of Edinburgh, 1994."},{"key":"5109768_CR2","unstructured":"Barras, B.: Auto-validation d'un syst\u00e8me de preuves avec families inductives, Ph.D. thesis, l'Universit\u00e9 Paris, 1997."},{"key":"5109768_CR3","unstructured":"Barras, B. et al.: The Coq Proof Assistant Reference Manual, version 6.3.1, 1999."},{"key":"5109768_CR4","unstructured":"Barras, B. and Werner, B.: Coq in Coq, 1997."},{"key":"5109768_CR5","doi-asserted-by":"crossref","unstructured":"Barthe, G., Ruys, M. and Barendregt, H.: A two-level approach towards lean proof-checking, in S. Berardi and M. Coppo (eds), Proceedings of Types '95, Lecture Notes in Comput. Sci. 1128, pp. 16\u201335.","DOI":"10.1007\/3-540-61780-9_59"},{"key":"5109768_CR6","doi-asserted-by":"crossref","unstructured":"Benaissa, Z., Briaud, D., Lescanne, P. and Rouyer-Degli, J.: \u03bbv, a calculus of explicit substitutions which preserves strong normalisation, Functional Programming\n6(5) (1996).","DOI":"10.1017\/S0956796800001945"},{"key":"5109768_CR7","doi-asserted-by":"crossref","unstructured":"van Benthem Jutting, L. S., McKinna, J. and Pollack, R.: Checking algorithms for pure type systems, in H. Barendregt and T. Nipkow (eds), Proceedings of the International Workshop on Types for Proofs and Programs, Lecture Notes in Comput. Sci. 806, Springer-Verlag, 1994, pp. 19\u201361.","DOI":"10.1007\/3-540-58085-9_71"},{"key":"5109768_CR8","first-page":"148","volume-title":"Proceedings CADE-17","author":"M. Bezem","year":"2000","unstructured":"Bezem, M., Hendriks, D. and de Nivelle, H.: Automated proof construction in type theory using resolution, in D. McAllester (ed.), Proceedings CADE-17, Lecture Notes in Comput. Sci. 1831, Springer-Verlag, Berlin, 2000, pp. 148\u2013163."},{"key":"5109768_CR9","doi-asserted-by":"crossref","unstructured":"Boutin, S.: Using reflection to build efficient and certified decision procedures, in M. Abadi and T. Ito (eds), Theoretical Aspects of Computer Software, Lecture Notes in Comput. Sci. 1281, Springer-Verlag, 1997, pp. 515\u2013529.","DOI":"10.1007\/BFb0014565"},{"issue":"5","key":"5109768_CR10","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"N. G. de Bruijn","year":"1972","unstructured":"de Bruijn, N. G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church\u2013Rosser theorem, Indag. Math. 34(5) (1972), 381\u2013392.","journal-title":"Indag. Math"},{"key":"5109768_CR11","unstructured":"Hendriks, D.: Clausification of first-order formulae, representation & correctness in type theory, Master's thesis, Utrecht University, 1998."},{"key":"5109768_CR12","unstructured":"Huet, G.: Residual theory in lambda calculus, a complete Gallina development, Rapport de recherche INRIA 2002, 1993."},{"key":"5109768_CR13","unstructured":"Matthes, R. and Joachimski, F.: Short proofs of normalization for the simply-typed lamdacalculus, permutative conversions and G\u00f6del's T, accepted for publication in the Arch. Math. Logic."},{"key":"5109768_CR14","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1007\/BFb0037113","volume-title":"Proceedings 1st Int. Conf. on Typed Lambda Calculi and Applications, TLCA'93","author":"J. McKinna","year":"1993","unstructured":"McKinna, J. and Pollack, R.: Pure type systems formalized, in M. Bezem and J. F. Groote (eds.), Proceedings 1st Int. Conf. on Typed Lambda Calculi and Applications, TLCA'93, Utrecht, The Netherlands, 16\u201318 March 1993, Vol. 664, Springer-Verlag, Berlin, 1993, pp. 289\u2013305."},{"issue":"3\u20134","key":"5109768_CR15","doi-asserted-by":"crossref","first-page":"373","DOI":"10.1023\/A:1006294005493","volume":"23","author":"J. McKinna","year":"1999","unstructured":"McKinna, J. and Pollack, R.: Some lambda calculus and type theory formalized, J. Automated Reasoning\n23(3\u20134) (1999), 373\u2013409.","journal-title":"J. Automated Reasoning"},{"key":"5109768_CR16","unstructured":"Persson, H.: Constructive completeness of intuitionistic predicate logic: A formalisation in type theory, Licentiate thesis, Chalmers University of Technology and University of G\u00f6tenborg, 1996."},{"key":"5109768_CR17","doi-asserted-by":"crossref","unstructured":"Pfenning, F.: The practice of logical frameworks, in H. Kirchner (ed.), Proceedings of the Colloquium on Trees in Algebra and Programming, Lecture Notes in Comput. Sci. 1059, Springer-Verlag, 1996, pp. 119\u2013134.","DOI":"10.1007\/3-540-61064-2_33"},{"key":"5109768_CR18","volume-title":"Termination of higher-order rewrite systems","author":"J. van de Pol","year":"1996","unstructured":"van de Pol, J.: Termination of higher-order rewrite systems, Ph.D. thesis, Utrecht University, Department of Philosophy, Utrecht, 1996."},{"key":"5109768_CR19","doi-asserted-by":"crossref","unstructured":"Prawitz, D.: Ideas and results in proof theory, in J. E. Fenstad (ed.), Proceedings of the Scandinavian Logic Symposium, North-Holland, Amsterdam, 1971, pp. 235\u2013307.","DOI":"10.1016\/S0049-237X(08)70849-8"},{"key":"5109768_CR20","unstructured":"Werner, B.: Une theorie des constructions inductives, Ph.D. thesis, l'Universit\u00e9 Paris, 1994."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1021923116629.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1021923116629\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1021923116629.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:41:31Z","timestamp":1749123691000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1021923116629"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,9]]},"references-count":20,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2002,9]]}},"alternative-id":["5109768"],"URL":"https:\/\/doi.org\/10.1023\/a:1021923116629","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2002,9]]}}}