{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:11:50Z","timestamp":1725664310980},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540617808"},{"type":"electronic","value":"9783540707226"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61780-9_72","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:25:32Z","timestamp":1330277132000},"page":"216-230","source":"Crossref","is-referenced-by-count":10,"title":["Circuits as streams in Coq: Verification of a sequential multiplier"],"prefix":"10.1007","author":[{"given":"Christine","family":"Paulin-Mohring","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"15_CR1","volume-title":"Research report, I3S","author":"L. Arditi","year":"1996","unstructured":"L. Arditi. Formal verification of microprocessors: a first experiment with the Coq proof assistant. Research report, I3S, Universit\u00e9 de Nice \u2014 Sophia Antipolis, 1996. To appear."},{"key":"15_CR2","unstructured":"R. S. Boyer and J. S. Moore. A computational logic. ACM Monograph. Academic Press, 1979."},{"key":"15_CR3","unstructured":"R. S. Boyer and J. S. Moore. A computational logic handbook. Academic Press, 1988."},{"key":"15_CR4","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 B. Werner. The Coq Proof Assistant Reference Manual version 5.10. Rapport Technique 0177, INRIA-Rocquencourt-CNRSENS Lyon, July 1995. Available by anonymous ftp on ftp.inria.fr."},{"key":"15_CR5","unstructured":"S. Coupet-Grimal and L. Jakubiec. Verification formelle de circuits avec Coq. In Journ\u00e9e du GDR-Programmation, Lille, September 1994. Also available as a Coq contribution."},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"S. Coupet-Grimal and L. Jakubiec. Coq and hardware verification: a case study. In International Conference on Theorem Proving in Higher Order Logics (TPHOL'96), Turku, Finland, August 1996. To appear.","DOI":"10.1007\/BFb0105401"},{"key":"15_CR7","unstructured":"H. Geuvers. Inductive and coinductive types with iteration and recursion. Faculty of Mathematics and Informatics, Catholic University Nijmegen, 1991."},{"key":"15_CR8","volume-title":"Projet Coq","author":"E. Gim\u00e9nez","year":"1995","unstructured":"E. Gim\u00e9nez. Co-inductive types in Coq. Technical report, Projet Coq, INRIA Rocquencourt, CNRS ENs Lyon, July 1995. To appear."},{"key":"15_CR9","volume-title":"Rapport de recherche","author":"E. Gim\u00e9nez","year":"1995","unstructured":"E. Gim\u00e9nez. Implementation of co-inductive types in Coq: an experiment with the alternating bit protocol. Rapport de recherche, LIP-ENS Lyon, 1995. In preparation."},{"key":"15_CR10","unstructured":"M. Gordon. Why higher-order logic is a good formalism for specifying and verifying hardware. In G. Milne and P. A. Subrahmanyam, editors, Formal Aspects of VLSI Design, 1986. also issued as University of Cambridge Computer Laboratory Technical Report No. 77, 1985."},{"key":"15_CR11","unstructured":"M.J.C. Gordon and T. F. Melham. Introduction to HOL. A theorem proving environment for higher order logic. University of Cambridge, 1993."},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"T. Hagino. A typed lambda-calculus with categorical type constructors. In D.H. Pitt, A. Poign\u00e9, and D.E. Rydeheard, editors, Category in Computer Science, volume 283 of Lecture Notes in Computer Science. Springer-Verlag, September 1987.","DOI":"10.1007\/3-540-18508-9_24"},{"key":"15_CR13","unstructured":"G. Huet, G. Kahn, and C. Paulin-Mohring. The Coq proof assistant \u2014 a tutorial. Rapport Technique 0178, Projet Coq-INRIA Rocquencourt-ENS Lyon, July 1995. Available by anonymous ftp on ftp.inria.fr."},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"F. Leclerc and C. Paulin-Mohring. Programming with streams in Coq. a case study: The sieve of eratosthenes. In H. Barendregt and T. Nipkow, editors, Types for Proofs and Programs, Types' 93, volume 806 of LNCS. Springer-Verlag, 1994.","DOI":"10.1007\/3-540-58085-9_77"},{"key":"15_CR15","unstructured":"G. C. Wraith. A note on categorical data types. In D.H. Pitt, D.E. Rydeheard, P. Dybjer, A.M. Pitts, and A. Poign\u00e9, editors, Category Theory and Computer Science, volume 389 of Lecture Notes in Computer Science, pages 118\u2013126. Springer-Verlag, September 1989."}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61780-9_72.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:10:56Z","timestamp":1605629456000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61780-9_72"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540617808","9783540707226"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-61780-9_72","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}