{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T16:31:54Z","timestamp":1725467514051},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540649878"},{"type":"electronic","value":"9783540498018"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0055148","type":"book-chapter","created":{"date-parts":[[2006,7,27]],"date-time":"2006-07-27T05:09:13Z","timestamp":1153976953000},"page":"387-399","source":"Crossref","is-referenced-by-count":10,"title":["Co-inductive axiomatization of a synchronous language"],"prefix":"10.1007","author":[{"given":"David","family":"Nowak","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean -Ren\u00e9","family":"Beauvais","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean -Pierre","family":"Talpin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,5,27]]},"reference":[{"key":"23_CR1","unstructured":"Bruno Barras and al. The Coq Proof Assistant Reference Manual. Technical report, INRIA, 1996."},{"key":"23_CR2","unstructured":"Saddek Bensalem, Paul Caspi, and Catherine Parent-Vigouroux. Handling dataflow programs in PVS. Research report (draft), Verimag, May 1996."},{"key":"23_CR3","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/0167-6423(91)90001-E","volume":"16","author":"A. Benveniste","year":"1991","unstructured":"Albert Benveniste, Paul Le Guernic, and Christian Jacquemot. 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":"23_CR4","unstructured":"G. Berry. The Constructive Semantics of Pure Esterel. Book in preparation, current version 2.0, http:\/\/zenon.inria.fr\/meije\/esterel."},{"key":"23_CR5","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/0167-6423(92)90005-V","volume":"19","author":"G. Berry","year":"1992","unstructured":"Gerard Berry and Georges Gonthier. The Esterel synchronous programming language: design, semantics, implementation. Science of Computer Programming, 19:87\u2013152, 1992.","journal-title":"Science of Computer Programming"},{"key":"23_CR6","doi-asserted-by":"crossref","unstructured":"C. Cornes and D. Terrasse. Inverting inductive predicates in Coq. In BRA Workshop on Types for Proofs and Programs (TYPES'95), volume 1158 of LNCS, 1996.","DOI":"10.1007\/3-540-61780-9_64"},{"key":"23_CR7","unstructured":"Thierry Gautier, Paul Le Guernic, and Fran\u00c7ois Dupont. Signal v4: manuel de r\u00e9f\u00e9rence (version pr\u00e9liminaire). Publication interne 832, IRISA, June 1994."},{"key":"23_CR8","unstructured":"Thierry Gautier, Paul Le Guernic, and Olivier Maffeis. For a New Real-Time Methodology. Research report, INRIA, 1994."},{"key":"23_CR9","doi-asserted-by":"crossref","unstructured":"Eduardo Gim\u00e9nez. An Application of Co-Inductive Types in Coq: Verification of the Alternating Bit Protocol. In Proceedings of the 1995 Workshop on Types for Proofs and Programs, number 1158 in LNCS, pages 135\u2013152. Springer Verlag, 1995.","DOI":"10.1007\/3-540-61780-9_67"},{"key":"23_CR10","unstructured":"Eduardo Gim\u00e9nez. Types Co-Inductifs et V\u00e9rification de Syst\u00e8mes R\u00e9actifs dans Coq. In Proceedings of the Journ\u00e9es du GDR Programmation, Grenoble, 1995."},{"key":"23_CR11","unstructured":"Eduardo Gim\u00e9nez. Un Calcul de Constructions Infinies et son Application \u00e0 la V\u00e9rification des Syst\u00e8mes Communicants. PhD thesis, Laboratoire de l'Informatique du Parall\u00e9lisme, Ecole Normale Sup\u00e9rieure de Lyon, December 1996."},{"key":"23_CR12","doi-asserted-by":"crossref","unstructured":"Andrew D. Gordon. The Formal Definition of a Synchronous Hardware-Description Language in Higher Order Logic. In Proceedings of the International Conference on Computer Design, pages 531\u2013534. IEEE Computer Society Press, October 1992.","DOI":"10.1109\/ICCD.1992.276230"},{"key":"23_CR13","unstructured":"Andrew D. Gordon. A Mechanised Definition of Silage in HOL. Research report 287, University of Cambridge Computer Laboratory, February 1993."},{"issue":"9","key":"23_CR14","doi-asserted-by":"publisher","first-page":"1305","DOI":"10.1109\/5.97300","volume":"79","author":"N. Halbwachs","year":"1991","unstructured":"N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. The synchronous dataflow programming language Lustre. Proc. of the IEEE, 79(9):1305\u20131320, September 1991.","journal-title":"Proc. of the IEEE"},{"key":"23_CR15","first-page":"270","volume":"number 1101","author":"M. Borgne Le","year":"1997","unstructured":"Michel Le Borgne, Herv\u00e9 Marchand, Eric Rutten, and Mazen Samaan. Formal Verification of Signal Programs: Application to a Power Transformer Station Controller. In Proc. of the 5th Int. Conf. on Algebraic Methodology and Software Technology (AMAST'96), number 1101 in LNCS, pages 270\u2013285, July 1997.","journal-title":"LNCS"},{"key":"23_CR16","unstructured":"Xavier Leroy. The Objective Caml system, release 1.07. Documentation and users's manual, INRIA, December 1997."},{"key":"23_CR17","unstructured":"F. Maraninchi. The Argos language: Graphical Representation of Automata and Description of Reactive Systems. In IEEE Workshop on Visual Languages, oct 1991."},{"issue":"1","key":"23_CR18","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1016\/0304-3975(91)90033-X","volume":"87","author":"R. Milner","year":"1991","unstructured":"Robin Milner and Mads Tofte. Co-induction in relational semantics. Theoretical Computer Science, 87(1):209\u2013220, 16 September 1991.","journal-title":"Theoretical Computer Science"},{"key":"23_CR19","unstructured":"David Nowak. http:\/\/www.irisa.fr\/prive\/nowak\/signal-coq\/. Coq code, IRISA, 1997."},{"key":"23_CR20","doi-asserted-by":"crossref","unstructured":"David Nowak, Jean-Pierre Talpin, Thierry Gautier, and Paul Le Guernic. An ML-Like Module System for the Synchronous Language Signal. In Proceedings of European Conference on Parallel Processing (Euro-Par'97), number 1300 in LNCS, pages 1244\u20131253. Springer Verlag, August 1997.","DOI":"10.1007\/BFb0002880"},{"key":"23_CR21","doi-asserted-by":"crossref","unstructured":"Christine Paulin-Mohring. Circuits as streams in Coq: Verification of a sequential multiplier. In S. Berardi and M. Coppo, editors, Types for Proofs and Programs, TYPES'95, volume 1158 of Lecture Notes in Computer Science, 1996.","DOI":"10.1007\/3-540-61780-9_72"},{"issue":"2\u20133","key":"23_CR22","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1016\/0167-6423(95)00017-8","volume":"25","author":"K. V. S. Prasad","year":"1995","unstructured":"K. V. S. Prasad. A calculus of broadcasting systems. Science of Computer Programming, 25(2\u20133):285\u2013327, December 1995.","journal-title":"Science of Computer Programming"},{"key":"23_CR23","unstructured":"B. Werner. Une Th\u00e9orie des Constructions Inductives. PhD thesis, Universit\u00e9 Paris VII, Mai. 1994."}],"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\/BFb0055148","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,20]],"date-time":"2019-04-20T04:34:30Z","timestamp":1555734870000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0055148"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540649878","9783540498018"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/bfb0055148","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}