{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T06:55:30Z","timestamp":1760079330231},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540412854"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/3-540-44404-1_12","type":"book-chapter","created":{"date-parts":[[2007,11,13]],"date-time":"2007-11-13T19:20:51Z","timestamp":1194981651000},"page":"179-188","source":"Crossref","is-referenced-by-count":6,"title":["A PVS Proof Obligation Generator for Lustre Programs"],"prefix":"10.1007","author":[{"given":"C\u00e8cile","family":"Canovas-Dumas","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paul","family":"Caspi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"12_CR1","unstructured":"J.-R. Abrial. The B-Book. Cambridge University Press, 1995. 187"},{"key":"12_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0053541","volume-title":"Foundations of Software Science and Computation Structures","author":"R. Amadio","year":"1998","unstructured":"R. Amadio and S. Coupet-Grimal. Analysis of a guard condition in type theory. In M. Nivat, editor, Foundations of Software Science and Computation Structures, volume 1378 of Lecture Notes in Computer Science. Springer Verlag, 1998. 179"},{"key":"12_CR3","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1137\/0205029","volume":"3","author":"E.A. Ashcroft","year":"1976","unstructured":"E.A. Ashcroft and W.W. Wadge. Lucid, a formal system for writing and proving programs. SIAM j. Comp., 3:336\u2013354, 1976. 187","journal-title":"SIAM j. Comp."},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"P. Caspi and M. Pouzet. A co-iterative characterization of synchronous stream functions. In Proceedings of the Workshop on Coalgebraic Methods in Computer Science, Lisbon, volume 11 of Electronic Notes in Theoretical Computer Science. Elsevier, 1998. 185","DOI":"10.1016\/S1571-0661(04)00050-7"},{"key":"12_CR5","series-title":"Lect Notes Comput Sci","volume-title":"Types for Proofs and Programs","author":"Th. Coquand","year":"1993","unstructured":"Th. Coquand. Infinite objects in type theory. In Types for Proofs and Programs, volume 806 of Lecture Notes in Computer Science. Springer Verlag, 1993. 179"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Th. Coquand and G. Huet. The calculus of construction. Information and Computation, 76(2), 1988. 179","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"12_CR7","series-title":"Lect Notes Comput Sci","volume-title":"Types for Proofs and Programs, TYPES\u201994","author":"E. Gimenez","year":"1995","unstructured":"E. Gimenez. Codifying guarded definitions with recursive schemes. In Types for Proofs and Programs, TYPES\u201994, volume 996 of Lecture Notes in Computer Science. Springer Verlag, 1995. 179"},{"issue":"9","key":"12_CR8","doi-asserted-by":"crossref","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 datafow programming language lustre. Proceedings of the IEEE, 79(9):1305\u20131320, September 1991. 179","journal-title":"Proceedings of the IEEE"},{"key":"12_CR9","unstructured":"U. Hensel and B. Jacobs. Coalgebraic theories of sequences in PVS. Technical Report CSI-R9708, Computer Science Institute, University of Nijmegen, 1997. 179"},{"key":"12_CR10","first-page":"229","volume":"62","author":"B. Jacobs","year":"1997","unstructured":"B. Jacobs and J. Rutten. A tutorial on (co)algebras and (co)induction. Bulletin of EATCS, 62:229\u2013259, 1997. 184","journal-title":"Bulletin of EATCS"},{"key":"12_CR11","unstructured":"G. Kahn. The semantics of a simple language for parallel programming. In IFIP 74. North Holland, 1974. 179"},{"key":"12_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-10235-3","volume-title":"A Calculus of Communicating Systems","author":"R. Milner","year":"1980","unstructured":"R. Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer Verlag, 1980. 179"},{"key":"12_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, Electronic Workshops in Computing, Bastad, Sweden, 1996. Springer-Verlag. 179","DOI":"10.14236\/ewic\/DCC1996.9"},{"key":"12_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/BFb0055148","volume-title":"Theorem Proving in Higher Order Logics","author":"D. Nowak","year":"1998","unstructured":"D. Nowak, J.R. Beauvais, and J.P. Talpin. Co-inductive axiomatization of a synchronous language. In Theorem Proving in Higher Order Logics, volume 1479 of Lecture Notes in Computer Science, pages 387\u2013399. Springer Verlag, 1998. 179, 185"},{"key":"12_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"PVS: a prototype verification system","author":"S. Owre","year":"1992","unstructured":"S. Owre, J. Rushby, and N. Shankar. PVS: a prototype verification system. In 11th Conf. on Automated Deduction, volume 607 of Lecture Notes in Computer Science, pages 748\u2013752. Springer Verlag, 1992. 179, 183"},{"key":"12_CR16","unstructured":"C. Paulin-Mohring. Circuits as streams in Coq, verification of a sequential multiplier. Research Report 95-16, Laboratoire de l'Informatique du Parall\u00e8lisme, September 1995. 179"},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"L. Paulson. Logic and Computation, Interactive Proof with Cambridge LCF. Cambridge University Press, 1987. 187","DOI":"10.1017\/CBO9780511526602"},{"key":"12_CR18","doi-asserted-by":"crossref","unstructured":"D. Pavlovi\u0107. Guarded induction on final coalgebras. In Proceedings of the Workshop on Coalgebraic Methods in Computer Science, Lisbon, volume 11 of Electronic Notes in Theoretical Computer Science, 1998. 187","DOI":"10.1016\/S1571-0661(04)00056-8"},{"key":"12_CR19","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0304-3975(90)90147-A","volume":"73","author":"P. Wadler","year":"1990","unstructured":"P. Wadler. Deforestation: transforming programs to eliminate trees. Theoretical Computer Science, 73:231\u2013248, 1990. 184","journal-title":"Theoretical Computer Science"}],"container-title":["Lecture Notes in Artificial Intelligence","Logic for Programming and Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44404-1_12.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:06:04Z","timestamp":1605647164000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44404-1_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540412854"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-44404-1_12","relation":{},"subject":[]}}