{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:30:36Z","timestamp":1774837836766,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540440390","type":"print"},{"value":"9783540456858","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45685-6_4","type":"book-chapter","created":{"date-parts":[[2007,5,19]],"date-time":"2007-05-19T16:47:53Z","timestamp":1179593273000},"page":"31-46","source":"Crossref","is-referenced-by-count":19,"title":["Efficient Reasoning about Executable Specifications in Coq"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pierre","family":"Courtieu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,25]]},"reference":[{"key":"4_CR1","unstructured":"C. Alvarado and Q.-H. Nguyen, elan for equational reasoning in coq. In J. Despeyroux, editor, Proceedings of LFM\u2019OO, 2000. Rapport Technique INRIA."},{"key":"4_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1007\/3-540-45418-7_2","volume-title":"Proceedings of e-SMART 2001","author":"G. Barthe","year":"2001","unstructured":"G. Barthe, G. Dufay, M. Huisman, and S. Melo de Sousa. Jakarta: a toolset to reason about the JavaCard platform. In I. Attali and T. Jensen, editors, Proceedings of e-SMART 2001, volume 2140 of Lecture Notes in Computer Science, pages 2\u201318. Springer-Verlag, 2001."},{"key":"4_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"32","DOI":"10.1007\/3-540-47813-2_3","volume-title":"Proceedings of VMCAI 2002","author":"G. Barthe","year":"2002","unstructured":"G. Barthe, G. Dufay, L. Jakubiec, and S. Melo de Sousa. A formal correspondence between offensive and defensive JavaCard virtual machines. In A. Cortesi, editor, Proceedings of VMCAI 2002, volume 2294 of Lecture Notes in Computer Science, pages 32\u201345. Springer-Verlag, 2002."},{"key":"4_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"302","DOI":"10.1007\/3-540-45309-1_20","volume-title":"Proceedings of ESOP 2001","author":"G. Barthe","year":"2001","unstructured":"G. Barthe, G. Dufay, L. Jakubiec, B. Serpette, and S. Melo de Sousa. A Formal Executable Semantics of the JavaCard Platform. In D. Sands, editor, Proceedings of ESOP 2001, volume 2028 of Lecture Notes in Computer Science, pages 302\u2013319. Springer-Verlag, 2001."},{"key":"4_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45842-5_2","volume-title":"Proceedings of TYPES 2000","author":"S. Berghofer","year":"2002","unstructured":"S. Berghofer and T. Nipkow. Executing higher order logic. In P. Callaghan, Z. Luo, J. McKinna, and R. Pollack, editors, Proceedings of TYPES 2000, volume LNCS 2277 of Lecture Notes in Computer Science. Springer-Verlag, 2002."},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"P. Borovansk\u00fd, H. Cirstea, H. Dubois, C. Kirchner, H. Kirchner, P.-E. Moreau, C. Ringeissen, and M. Vittek. The Elan VS.4. Manual, 2000.","DOI":"10.1016\/S1571-0661(04)00032-5"},{"key":"4_CR7","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1006\/jsco.1996.0076","volume":"23","author":"A. Bouhoula","year":"1997","unstructured":"A. Bouhoula. Automated theorem proving by test set induction. Journal of Symbolic Computation, 23:47\u201377, 1997.","journal-title":"Journal of Symbolic Computation"},{"key":"4_CR8","unstructured":"R.S. Boyer and J.S. Moore. A Computational Logic Handbook. Academic Press, 1988."},{"key":"4_CR9","unstructured":"Coq Development Team. The Coq Proof Assistant User\u2019s Guide. Version 1.2, January 2002."},{"key":"4_CR10","unstructured":"C. Cornes. Conception d\u2019un langage de haut niveau de representation de preuves: R\u00e9currence par filtrage de motifs; Unification en pr\u00e9sence de types inductifs primitifs; Synth\u00e8se de lemmes d\u2019inversion. PhD thesis, Universit\u00e9 de Paris 7, 1997."},{"key":"4_CR11","series-title":"Lect Notes Comput Sci","first-page":"85","volume-title":"Proceedings of Types\u201995","author":"C. Cornes","year":"1995","unstructured":"C. Cornes and D. Terrasse. Automating inversion and inductive predicates in Coq. In S. Berardi and M. Coppo, editors, Proceedings of Types\u201995, volume 1158 of Lecture Notes in Computer Science, pages 85\u2013104. Springer-Verlag, 1995."},{"key":"4_CR12","unstructured":"P. Courtieu. Function Schemes in Coq: Documentation and tutorial. See http:\/\/www-sop.inria.fr\/lemme\/Pierre.Courtieu\/funscheme.html"},{"key":"4_CR13","unstructured":"M.J.C. Gordon and T.F. Melham, editors. Introduction to HOL: A theorem proving environment for higher-order logic. Cambridge University Press, 1993."},{"key":"4_CR14","series-title":"Lect Notes Comput Sci","first-page":"85","volume-title":"Proceedings of CARDIS\u201998","author":"J.-L. Lanet","year":"1998","unstructured":"J.-L. Lanet and A. Requet. Formal Proof of Smart Card Applets Correctness. In J.-J. Quisquater and B. Schneier, editors, Proceedings of CARDIS\u201998, volume 1820 of Lecture Notes in Computer Science, pages 85\u201397. Springer-Verlag, 1998."},{"key":"4_CR15","unstructured":"Z. Luo and R. Pollack. LEGO proof development system: User\u2019s manual. Technical Report ECS-LFCS-92-211, LFCS, University of Edinburgh, May 1992."},{"key":"4_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"328","DOI":"10.1007\/BFb0037116","volume-title":"Proceedings of TLCA\u2019 93","author":"C. Paulin-Mohring","year":"1993","unstructured":"C. Paulin-Mohring. Inductive definitions in the system Coq. Rules and properties. In M. Bezem and J.F. Groote, editors, Proceedings of TLCA\u2019 93, volume 664 of Lecture Notes in Computer Science, pages 328\u2013345. Springer-Verlag, 1993."},{"key":"4_CR17","unstructured":"C. Paulin-Mohring. D\u00e9finitions Inductives en Theorie des Types d\u2019Ordre Superieur. Habilitation \u00e0 diriger les recherches, Universit\u00e9 Claude Bernard Lyon I, 1996."},{"key":"4_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A generic theorem prover","author":"L. Paulson","year":"1994","unstructured":"L. Paulson. Isabelle: A generic theorem prover, volume 828 of Lecture Notes in Computer Science. Springer-Verlag, 1994."},{"key":"4_CR19","doi-asserted-by":"crossref","unstructured":"F. Pfenning. Elf: a meta-language for deductive systems. In A. Bundy, editor, Proceedings of CADE-12, volume 814 of Lecture Notes in Artificial Intelligence, pages 811\u2013815. Springer-Verlag, 1994.","DOI":"10.1007\/3-540-58156-1_66"},{"key":"4_CR20","unstructured":"K. Slind. Reasoning about Terminating Functional Programs. PhD thesis, TU M\u00fcnich, 1999."},{"key":"4_CR21","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"230","DOI":"10.1007\/3-540-60043-4_56","volume-title":"Proceedings of AMAST\u201995","author":"D. Terrasse","year":"1995","unstructured":"D. Terrasse. Encoding natural semantics in Coq. In V. S. Alagar, editor, Proceedings of AMAST\u201995, volume 936 of Lecture Notes in Computer Science, pages 230\u2013244. Springer-Verlag, 1995."},{"key":"4_CR22","unstructured":"D. Terrasse. Vers un environnement d\u2019aide au d\u00e9veloppement de preuves en S\u00e9mantique Naturelle. PhD thesis, Ecole Nationale des Ponts et Chauss\u00e9es, 1995."}],"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-45685-6_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T01:38:09Z","timestamp":1556415489000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45685-6_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540440390","9783540456858"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-45685-6_4","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]}}}