{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,14]],"date-time":"2024-09-14T09:04:01Z","timestamp":1726304641795},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540615873"},{"type":"electronic","value":"9783540706410"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/bfb0105401","type":"book-chapter","created":{"date-parts":[[2011,11,9]],"date-time":"2011-11-09T21:17:00Z","timestamp":1320873420000},"page":"125-139","source":"Crossref","is-referenced-by-count":14,"title":["Coq and hardware verification: A case study"],"prefix":"10.1007","author":[{"given":"Solange","family":"Coupet-Grimal","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Line","family":"Jakubiec","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2007,4,29]]},"reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"M. Aagaard and M. Leeser. A Methodology for Reusable Hardware Proofs. In International Workshop on Higher Order Logic Theorem Proving and its Applications, 1992.","DOI":"10.1016\/B978-0-444-89880-7.50018-8"},{"key":"9_CR2","unstructured":"M. Allemand. Mod\u00e9lisation Formelle et Preuve de Circuits avec LP. PhD thesis, Universit\u00e9 de Provence, July 1995."},{"key":"9_CR3","unstructured":"L. Arditi. Formal Verification of Microprocessors: a First Experiment with the Coq Proof Assistant. Research Report I3S\/Universit\u00e9 de Nice-Sophia Antipolis. RR-96-31, 1996."},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"J. Bertot and Y. Bertot. Ctcoq: a System Presentation. In CADE-13, 1996.","DOI":"10.1007\/3-540-61511-3_85"},{"key":"9_CR5","unstructured":"R. S. Boyer and J. S. Moore. A computational logic handbook. Academic Press Inc., 1988."},{"key":"9_CR6","unstructured":"A. Camilleri, M. Gordon, and T. Melham. Hardware Verification Using Higher Order Logic. In From HDL Descriptions to Guaranteed Correct Circuit Designs. Elsevier Scientific Publishers, 1987."},{"key":"9_CR7","unstructured":"T. Coquand. Une Th\u00e9orie des Constructions. PhD thesis, Universit\u00e9 Paris 7, Janvier 1989."},{"key":"9_CR8","doi-asserted-by":"crossref","unstructured":"T. Coquand and G. Huet. Constructions: A Higher Order Proof System For Mechanizing Mathematics. In EUROCAL'85, number 203 in LNCS. Springer-Verlag, 1985.","DOI":"10.1007\/3-540-15983-5_13"},{"key":"9_CR9","unstructured":"C. Cornes, J. Courant, J.-C. Filli\u00e2tre, G. Huet, P. Manoury, C. Mu\u00f1oz, C. Murthy, C. Parent, C. Paulin-Mohring, A. Sa\u00efbi, and W. Benjamin. The Coq Proof Assistant Reference Manual. Technical report, INRIA-Rocquencourt, CNRS-ENS Lyon, Feb. 1996."},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Y. Coscoy, G. Kahn, and L. Th\u00e9ry. Extracting Text from Proof. In Typed Lambda-Calculi and Applications, number 905 in LNCS. Springer-Verlag, April 1995.","DOI":"10.1007\/BFb0014048"},{"key":"9_CR11","unstructured":"S. Coupet-Grimal and L. Jakubiec. V\u00e9rification Formelle de Circuits avec COQ. In Journ\u00e9es du GDR Programmation, Sept. 1994."},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"J.-Y. Girard. The System F of Variable Types, Fifteen Years Later. Theoretical Computer Science 45, 1986.","DOI":"10.1016\/0304-3975(86)90044-7"},{"key":"9_CR13","unstructured":"M. Gordon. LCF-LSM. Technical Report 41, University of Cambridge, 1984."},{"key":"9_CR14","unstructured":"M. Gordon. Why Higher-Order Logic is a Good Formalism for Specifying and Verifying Hardware. Technical Report 77, University of Cambridge Computer Laboratory, 1986. edited by G. Milne and P. A. Subrahmanyam, North Holland."},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"M. Gordon, R. Milner, and C. Wadsworth. Edinburgh LCF: A Mechanized Logic of Computation, volume 78 of LNCS. Springer-Verlag, Department of Computer Science, University of Edinburgh, 1979.","DOI":"10.1007\/3-540-09724-4"},{"issue":"9","key":"9_CR16","doi-asserted-by":"publisher","first-page":"949","DOI":"10.1109\/32.58783","volume":"16","author":"F. Hanna","year":"1990","unstructured":"F. Hanna, N. Daeche, and M. Longley. Specification and Verification Using Dependent Types. IEEE Transactions on Software Engineering, 16(9):949\u2013964, Sept. 1990.","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"4","key":"9_CR17","doi-asserted-by":"crossref","first-page":"429","DOI":"10.1007\/BF00243132","volume":"5","author":"W. A. Hunt","year":"1989","unstructured":"W. A. Hunt. Microprocessor Design Verification. Journal of Automated Reasonning, 5(4):429\u2013460, 1989.","journal-title":"Journal of Automated Reasonning"},{"key":"9_CR18","unstructured":"M. Leeser. Using Nuprl for the Verification and Synthesis of Hardware. In C. A. R. Hoare and M. J. C. Gordon, editors, Mechanized Reasoning and Hardware Design, International Series on Computer Science. Prentice Hall, 1992."},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"S. Owre, J. Rushby, N. Shankar, and M. Srivas. A Tutorial on Using PVS for Hardware Verification. In 2nd International Conference on Theorem Provers in Circuit Design, number 901 in LNCS, pages 258\u2013279. Springer Verlag, Sept. 1994.","DOI":"10.1007\/3-540-59047-1_53"},{"key":"9_CR20","unstructured":"C. Parent. Synth\u00e8se de Preuves de Programmes dans le Calcul des Constructions Inductives. PhD thesis, Ecole Normale Sup\u00e9rieure de Lyon, Janvier 1995."},{"key":"9_CR21","unstructured":"C. Paulin. Extraction de Programmes dans Coq. PhD thesis, Universit\u00e9 Paris 7, Janvier 1989."},{"key":"9_CR22","unstructured":"C. Paulin-Mohring. Inductive Definitions in the System Coq: Rules and Properties. Research Report 92-49, Ecole Normale Sup\u00e9rieure de Lyon, 1992."},{"key":"9_CR23","doi-asserted-by":"crossref","unstructured":"C. Paulin-Mohring. Circuits as Streams in Coq. Verification of a Sequential Multiplier. Basic Research Action \u201dTypes\u201d, Juillet 1995.","DOI":"10.1007\/3-540-61780-9_72"},{"key":"9_CR24","doi-asserted-by":"crossref","unstructured":"J. B. Saxe, S. J. Garland, J. V. Guttag, and J. J. Horning. Using Transformations and Verification in Circuit Design. Formal Methods in System Design, (3):181\u2013209, Dec. 1993.","DOI":"10.1007\/BF01384073"},{"key":"9_CR25","doi-asserted-by":"crossref","unstructured":"M. K. Srivas and S. P. Miller. Applying Formal Verification to a Commercial Microprocessor. IFIP International Conference on Computer Hardware Description Languages, Aug. 1995.","DOI":"10.1109\/ASPDAC.1995.486361"}],"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\/BFb0105401","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,27]],"date-time":"2020-06-27T09:22:54Z","timestamp":1593249774000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0105401"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540615873","9783540706410"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/bfb0105401","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}