{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,29]],"date-time":"2026-09-29T02:22:03Z","timestamp":1790648523507,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540429579","type":"print"},{"value":"9783540456537","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45653-8_34","type":"book-chapter","created":{"date-parts":[[2007,6,9]],"date-time":"2007-06-09T04:57:30Z","timestamp":1181365050000},"page":"495-506","source":"Crossref","is-referenced-by-count":7,"title":["Certifying Synchrony for Free"],"prefix":"10.1007","author":[{"given":"Sylvain","family":"Boulm\u00e9","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Gr\u00e9goire","family":"Hamon","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2001,11,20]]},"reference":[{"key":"34_CR1","unstructured":"Barras B, et al. The Coq Proof Assistant Reference Manual, version 6.3.1. Coq Project, INRIA-Rocquencourt, May 2000."},{"key":"34_CR2","doi-asserted-by":"crossref","unstructured":"Bensalem S, et al. A methodology for proving control programs with Lustre and PVS. In Dependable Computingfor Critical Applications, DCCA-7. IEEE Computer Society, January 1999.","DOI":"10.1109\/DCFTS.1999.814291"},{"key":"34_CR3","unstructured":"Boulm\u00e9 S and Hamon G. A clocked denotational semantics for Lucid-Synchrone in Coq. Technical report, LIP6, 2001. Available at \n                    http:\/\/www-spi.lip6.fr\/lucid-synchrone\/lucid_in_coq_report.ps\n                    \n                  ."},{"key":"34_CR4","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/0167-6423(91)90001-E","volume":"16","author":"A. Benveniste","year":"1991","unstructured":"Benveniste A, et al. Synchronous programming with events and relations: The Signal language and its semantics. Science of Computer Programming, 16:103\u2013149, 1991.","journal-title":"Science of Computer Programming"},{"key":"34_CR5","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/0304-3975(92)90326-B","volume":"94","author":"P. Caspi","year":"1992","unstructured":"Caspi P. Clocks in dataflow languages. Theorical Computer Science, 94:125\u2013140, 1992.","journal-title":"Theorical Computer Science"},{"key":"34_CR6","series-title":"Lect Notes Comput Sci","volume-title":"TPHOLs\u201999","author":"S. Coupet-Grimal","year":"1999","unstructured":"Coupet-Grimal S and Jakubiec L. Hardware veri.cation using coinduction in Coq. In TPHOLs\u201999, number 1690 in LNCS. 1999."},{"key":"34_CR7","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"1988","unstructured":"Coquand T and Huet G. The Calculus of Constructions. Information and Computation, 76:95\u2013120, 1988.","journal-title":"Information and Computation"},{"key":"34_CR8","doi-asserted-by":"crossref","unstructured":"Caspi P and Pouzet M. A co-iterative characterization of synchronous stream functions. In Coalgebraic Methods in Computer Science (CMCS\u201998), ENTCS. 28\u201329 March 1998.","DOI":"10.1016\/S1571-0661(04)00050-7"},{"key":"34_CR9","unstructured":"Caspi P and Pouzet M. Lucid Synchrone, an ML extension to Lustre. In Submited for publication. 2000."},{"key":"34_CR10","unstructured":"Colaco JL and Pouzet M. Prototypages. Rapport final du projet GENIE II, Verilog SA, Janvier 2000."},{"key":"34_CR11","unstructured":"Dumas-Canovas C and Caspi P. A PVS proof obligation generator for Lustre programs. In LPAR\u20192000, number 1955 in LNAI. 2000."},{"key":"34_CR12","unstructured":"Filli\u00e2tre JC. Preuve de programmes imp\u00e9ratifs en th\u00e9orie des types. Ph.D. thesis, Universit\u00e9 Paris-Sud, July 1999."},{"key":"34_CR13","unstructured":"Gimenez E. Codifying guarded definitions with recursive schemes. Technical Report 95-07, LIP ENS-Lyon, December 1994."},{"key":"34_CR14","unstructured":"Gimenez E. A tutorial on recursive types in Coq. Technical Report 0221, INRIA, May 1998."},{"key":"34_CR15","doi-asserted-by":"crossref","unstructured":"Halbwachs N. Synchronous programming of reactive systems. Kluwer Academic Pub., 1993.","DOI":"10.1007\/978-1-4757-2231-4"},{"issue":"9","key":"34_CR16","doi-asserted-by":"publisher","first-page":"1305","DOI":"10.1109\/5.97300","volume":"79","author":"N. Halbwachs","year":"1991","unstructured":"Halbwachs N, et al. The Synchronous data.ow programming language Lustre. Proceedings of the IEEE, 79(9):1305\u20131320, September 1991.","journal-title":"Proceedings of the IEEE"},{"key":"34_CR17","series-title":"Lect Notes Comput Sci","volume-title":"TPHOLs\u20192000","author":"M. Kerboeuf","year":"2000","unstructured":"Kerboeuf M, et al. The steam-boiler problem in Signal-Coq. In TPHOLs\u20192000, number 1869 in LNCS. 2000."},{"key":"34_CR18","series-title":"Lect Notes Comput Sci","volume-title":"TPHOLs\u201998","author":"D. Nowak","year":"1998","unstructured":"Nowak D, et al. Co-inductive axiomatization of a synchronous language. In TPHOLs\u201998, number 1479 in LNCS. 1998."},{"key":"34_CR19","series-title":"Lect Notes Comput Sci","volume-title":"Mathematics for Programs Constructions\u201995","author":"C. Parent","year":"1995","unstructured":"Parent C. Synthesizing proofs from programs in the Calculus of Inductive Constructions. In Mathematics for Programs Constructions\u201995, number 947 in LNCS. 1995."},{"key":"34_CR20","unstructured":"Pouzet M, et al. Lucid Synchrone v2.0-Tutorial and Reference manual. LIP6, April 2001. Available at \n                    http:\/\/www-spi.lip6.fr\/lucidsynchrone\/lucid_synchrone_2.0_manual.ps\n                    \n                  ."},{"key":"34_CR21","series-title":"Lect Notes Comput Sci","volume-title":"TLCA","author":"C. Paulin-Mohring","year":"1993","unstructured":"Paulin-Mohring C. Inductive De.nitions in the System Coq-Rules and Properties. In TLCA, number 664 in LNCS. 1993."},{"key":"34_CR22","unstructured":"Telelogic. Telelogic Tau Scade language-Reference manual, 2001."}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45653-8_34","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,17]],"date-time":"2019-02-17T07:52:49Z","timestamp":1550389969000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45653-8_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540429579","9783540456537"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-45653-8_34","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2001]]}}}