{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,14]],"date-time":"2024-09-14T09:07:29Z","timestamp":1726304849636},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540664635"},{"type":"electronic","value":"9783540482567"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48256-3_7","type":"book-chapter","created":{"date-parts":[[2007,8,3]],"date-time":"2007-08-03T20:15:22Z","timestamp":1186172122000},"page":"91-108","source":"Crossref","is-referenced-by-count":2,"title":["Hardware Verification Using Co-induction in COQ"],"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":[[1999,9,17]]},"reference":[{"key":"7_CR1","volume-title":"Technical Report 0203, INRIA-Rocquencourt","author":"B. Barrasal","year":"1997","unstructured":"B. Barras and al. The Coq Proof Assistant Reference Manual: Version 6.1. Technical Report 0203, INRIA-Rocquencourt, CNRS-ENS Lyon, France, Dec. 1997."},{"key":"7_CR2","volume-title":"Technical Report 97-48","author":"D. Cachera","year":"1997","unstructured":"D. Cachera. Verification of Arithmetic Circuits using a Functional Language and PVS. Technical Report 97-48, ENS-Lyon, LIP, Dec. 1997."},{"key":"7_CR3","unstructured":"T. Coquand. Une Th\u00e9orie des Constructions. PhD thesis, Universit\u00e9 Paris 7, Janvier 1989."},{"key":"7_CR4","series-title":"Lect Notes Comput Sci","volume-title":"EUROCAL 85, Linz Springer-Verlag","author":"T. Coquand","year":"1985","unstructured":"T. Coquand and G. Huet. Constructions: A Higher Order Proof System for Mechanizing Mathematics. EUROCAL 85, Linz Springer-Verlag LNCS 203, 1985."},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"S. Coupet-Grimal and L. Jakubiec. Coq and Hardware Verification: a Case Study. In J. G. J. vonWright and J. Harrison, editors, TPHOLs\u201996, LCNS 1125, pages 125\u2013139, Turku (Finlande), 27\u201330th August 1996. Springer-Verlag.","DOI":"10.1007\/BFb0105401"},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"P. Curzon. The Formal Verification of the Fairisle ATM Switching Element. Technical Report 329, University of Cambridge, Mar. 1994.","DOI":"10.1145\/197917.198171"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"P. Curzon. The Formal Verification of the Fairisle ATM Switching Element: an Overview. Technical Report 328, University of Cambridge, Mar. 1994.","DOI":"10.1145\/197917.198171"},{"key":"7_CR8","unstructured":"E. Garcez and W. Rosenstiel. The Verification of an ATM Switching Fabric using the HSIS Tool. IX Brazilian Symposium on the Design of Integrated Circuits, 1996."},{"key":"7_CR9","unstructured":"E. Gim\u00e9nez. Un calcul de constructions in finies et son application \u00e0 la v\u00e8rication de syst\u00e8mes communicants. PhD thesis, Ecole Normale Superieure de Lyon, 1996."},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"I. Leslie and D. McAuley. Fairisle: A General Topology ATM LAN. http:\/\/www.cl.cam.ac.uk\/Research\/SRG\/fairpap.html , Dec. 1990.","DOI":"10.1145\/115992.116022"},{"issue":"19","key":"7_CR11","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1145\/115994.116022","volume":"4","author":"I. Leslie","year":"1991","unstructured":"I. Leslie and D. McAuley. Fairisle: An ATM Network for the Local Area. ACM Communication Review, 4(19):327\u2013336, September 1991.","journal-title":"ACM Communication Review"},{"key":"7_CR12","unstructured":"J. Lu and S. Tahar. Practical Approaches to the Automatic Verification of an ATM Switch using VIS. In IEEE 8th Great Lakes Symposium on VLSI (GLS-VLSI\u201998), pages 368\u2013373, Lafayette, Louisiana, USA, Feb. 1998. IEEE Computer Society Press."},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"P. S. Miner and S. D. Johnson. Verification of an Optimized Fault-Tolerant Clock Synchronization Circuit. In Designing Correct Circuits. B\u00e4stad, 1996.","DOI":"10.14236\/ewic\/DCC1996.9"},{"key":"7_CR14","unstructured":"C. Paulin-Mohring. Inductive Definition in the System Coq: Rules and Properties. Typed Lambda Calculi and Applications (Also Research Report 92-49, LIPENS Lyon), Dec. 1993."},{"key":"7_CR15","doi-asserted-by":"crossref","unstructured":"C. Paulin-Mohring. Circuits as Streams in Coq. Verification of a Sequential Multiplier. Basic Research Action \u201cTypes\u201d, July 1995.","DOI":"10.1007\/3-540-61780-9_72"},{"key":"7_CR16","doi-asserted-by":"crossref","unstructured":"S. Tahar and P. Curzon. A Comparison of MDG and HOL for Hardware Verification. In J. G. J. von Wright and J. Harrison, editors, TPHOLs\u201996, LCNS 1125, pages 415\u2013430, Turku (Finlande), 27\u201330th August 1996. Springer-Verlag.","DOI":"10.1007\/BFb0105419"},{"key":"7_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1007\/3-540-49519-3_28","volume-title":"Formal Methods in Computer-Aided Design","author":"S. Tahar","year":"1998","unstructured":"S. Tahar, P. Curzon, and Lu. J. Three Approaches to Hardware Verification: HOL, MDG and VIS Compared. In G. Gopalakrishnan and P. Windley, editors, Formal Methods in Computer-Aided Design, LNCS 1522, pages 433\u2013450, FMCAD\u201998, Palo Alto, California, USA, Nov. 1998. Springer-Verlag."},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"S. Tahar, Z. Zhou, X. Song, E. Cerny, and M. Langevin. Formal Verification of an ATM Switch Fabric using Multiway Decision Graphs. In Proc. of the Great Lakes Symp. on VLSI, IEEE Computer Society Press, pages 106\u2013111, Mar. 1996.","DOI":"10.1109\/GLSV.1996.497603"}],"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-48256-3_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,21]],"date-time":"2021-08-21T05:46:47Z","timestamp":1629524807000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48256-3_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540664635","9783540482567"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-48256-3_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1999]]}}}