{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T06:55:10Z","timestamp":1747810510649},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540440390"},{"type":"electronic","value":"9783540456858"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45685-6_21","type":"book-chapter","created":{"date-parts":[[2007,5,19]],"date-time":"2007-05-19T16:47:53Z","timestamp":1179593273000},"page":"314-331","source":"Crossref","is-referenced-by-count":12,"title":["Proving the Equivalence of Microstep and Macrostep Semantics"],"prefix":"10.1007","author":[{"given":"Klaus","family":"Schneider","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,7,25]]},"reference":[{"key":"21_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1040","volume":"111","author":"L. Aceto","year":"1994","unstructured":"L. Aceto, B. Bloom, and F. Vaandrager. Turning SOS rules into equations. Information and Computation, 111:1\u201352, 1994.","journal-title":"Information and Computation"},{"key":"21_CR2","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1016\/B978-044482830-9\/50021-7","volume-title":"Handbook of Process Algebra","author":"L. Aceto","year":"2001","unstructured":"L. Aceto, W. Fokkink, and C. Verhoef. Structural operational semantics. In J. Bergstra, A. Ponse, and S. Smolka, editors, Handbook of Process Algebra, pages 197\u2013292. Elsevier, Amsterdam, 2001."},{"key":"21_CR3","series-title":"Lect Notes Comput Sci","first-page":"87","volume-title":"Higher Order Logic Theorem Proving and Its Applications","author":"C. Angelo","year":"1993","unstructured":"C. Angelo, L. Claesen, and H. D. Man. Degrees of Formality in Shallow Embedding Hardware Description Languages in HOL. In J. Joyce and C.-J. Seger, editors, Higher Order Logic Theorem Proving and Its Applications, volume 780 of LNCS, pages 87\u201399, Vancouver, Canada, August 1993. University of British Columbia, Springer-Verlag, published 1994."},{"key":"21_CR4","unstructured":"G. Berry. A hardware implementation of pure Esterel. In ACM International Workshop on Formal Methods in VLSI Design, Miami, Florida, January 1991."},{"key":"21_CR5","unstructured":"G. Berry. The foundations of Esterel. In G. Plotkin, C. Stirling, and M. Tofte, editors, Proof, Language and Interaction: Essays in Honour of Robin Milner. MIT Press, 1998."},{"key":"21_CR6","unstructured":"G. Berry. The constructive semantics of pure Esterel, July 1999."},{"key":"21_CR7","unstructured":"G. Berry. The Esterel v5_91 language primer. \n                    http:\/\/www.esterel.org\n                    \n                  , June 2000."},{"issue":"2","key":"21_CR8","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/0167-6423(92)90005-V","volume":"19","author":"G. Berry","year":"1992","unstructured":"G. Berry and G. Gonthier. The Esterel synchronous programming language: Design, semantics, implementation. Science of Computer Programming, 19(2):87\u2013152, 1992.","journal-title":"Science of Computer Programming"},{"key":"21_CR9","unstructured":"R. Boulton. A HOL semantics for a subset of ELLA. technical report 254, University of Cambridge, Computer Laboratory, April 1992."},{"key":"21_CR10","unstructured":"R. Boulton, A. Gordon, M. Gordon, J. Herbert, and J. van Tassel. Experience with embedding hardware description languages in HOL. In International Conference on Theorem Provers in Circuit Design (TPCD), pages 129\u2013156, Nijmegen, June 1992. IFIP TC10\/WG 10.2, North-Holland."},{"key":"21_CR11","volume-title":"Research Report 3487","author":"F. Boussinot","year":"1998","unstructured":"F. Boussinot. SugarCubes implementation of causality. Research Report 3487, Institut National de Recherche en Informatique et en Automatique (INRIA), Sophia Antipolis Cedex (France), September 1998."},{"key":"21_CR12","doi-asserted-by":"crossref","unstructured":"J. Brzozowski and C.-J. Seger. Asynchronous Circuits. Springer Verlag, 1995.","DOI":"10.1007\/978-1-4612-4210-9"},{"key":"21_CR13","series-title":"Lect Notes Comput Sci","first-page":"338","volume-title":"Higher Order Logic Theorem Proving and its Applications","author":"N. Day","year":"1993","unstructured":"N. Day and J. Joyce. The semantics of statecharts in HOL. In J. Joyce and C.-J. Seger, editors, Higher Order Logic Theorem Proving and its Applications, volume 780 of LNCS, pages 338\u2013352, Vancouver, Canada, August 1993. University of British Columbia, Springer-Verlag, published 1994."},{"key":"21_CR14","unstructured":"Esterel-Technology. Website. \n                    http:\/\/www.esterel-technologies.com\n                    \n                  ."},{"key":"21_CR15","unstructured":"A. Girault and G. Berry. Circuit generation and verification of Esterel programs. Research report 3582, INRIA, December 1998."},{"key":"21_CR16","unstructured":"M. Gordon and T. Melham. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993."},{"key":"21_CR17","unstructured":"N. Halbwachs and F. Maraninchi. On the symbolic analysis of combinational loops in circuits and synchronous programs. In Euromicro Conference, Como, Italy, September 1995."},{"key":"21_CR18","unstructured":"Jester Home Page. Website. \n                    http:\/\/www.parades.rm.cnr.it\/projects\/jester\/jester.html\n                    \n                  ."},{"key":"21_CR19","doi-asserted-by":"crossref","unstructured":"L. Lavagno and E. Sentovich. ECL: A specification environment for system-level design. In ACM\/IEEE Design Automation Conference (DAC), 1999.","DOI":"10.1145\/309847.309989"},{"key":"21_CR20","doi-asserted-by":"crossref","unstructured":"G. Logothetis and K. Schneider. Extending synchronous languages for generating abstract real-time models. In European Conference on Design, Automation and Test in Europe (DATE), Paris, France, March 2002. IEEE Computer Society.","DOI":"10.1109\/DATE.2002.998390"},{"issue":"7","key":"21_CR21","doi-asserted-by":"crossref","first-page":"950","DOI":"10.1109\/43.293952","volume":"13","author":"S. Malik","year":"1994","unstructured":"S. Malik. Analysis of cycle combinational circuits. IEEE Transactions on Computer Aided Design, 13(7):950\u2013956, July 1994.","journal-title":"IEEE Transactions on Computer Aided Design"},{"key":"21_CR22","volume-title":"Technical Report 146","author":"T. Melham","year":"1988","unstructured":"T. Melham. Automating recursive type definitions in higher order logic. Technical Report 146, University of Cambridge Computer Laboratory, Cambridge CB2 3QG, England, September 1988."},{"key":"21_CR23","unstructured":"G. Plotkin. A Structural Approach to Operational Semantics. Technical Report FN-19, DAIMI, Aarhus University, 1981."},{"key":"21_CR24","volume-title":"Arbeitspapiere 964","author":"A. Poign\u00e9","year":"1995","unstructured":"A. Poign\u00e9 and L. Holenderski. Boolean automata for implementing pure Esterel. Arbeitspapiere 964, GMD, Sankt Augustin, 1995."},{"key":"21_CR25","unstructured":"POLIS Homepage. Website. \n                    http:\/\/www-cad.eecs.berkeley.edu\/\n                    \n                  ."},{"key":"21_CR26","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1007\/3-540-60275-5_71","volume-title":"Higher Order Logic Theorem Proving and its Applications","author":"R. Reetz","year":"1995","unstructured":"R. Reetz. Deep Embedding VHDL. In E. Schubert, P. Windley, and J. Alves-Foss, editors, Higher Order Logic Theorem Proving and its Applications, volume 971 of LNCS, pages 277\u2013292, Aspen Grove, Utah, USA, September 1995. Springer-Verlag."},{"key":"21_CR27","unstructured":"F. Rocheteau and N. Halbwachs. Pollux, a Lustre-based hardware design environment. In P. Quinton and Y. Robert, editors, Conference on Algorithms and Parallel VLSI Architectures II, Chateau de Bonas, 1991."},{"key":"21_CR28","first-page":"205","volume-title":"International IFIP Workshop on Distributed and Parallel Embedded Systems","author":"K. Schneider","year":"2000","unstructured":"K. Schneider. A verified hardware synthesis for Esterel. In F. Rammig, editor, International IFIP Workshop on Distributed and Parallel Embedded Systems, pages 205\u2013214, Schlo\u00df Ehringerfeld, Germany, 2000. Kluwer Academic Publishers."},{"key":"21_CR29","doi-asserted-by":"crossref","unstructured":"K. Schneider. Embedding imperative synchronous languages in interactive theorem provers. In International Conference on Application of Concurrency to System Design (ICACSD 2001), pages 143\u2013156, Newcastle upon Tyne, UK, June 2001. IEEE Computer Society Press.","DOI":"10.1109\/CSD.2001.981772"},{"key":"21_CR30","doi-asserted-by":"crossref","unstructured":"K. Schneider and M. Wenz. A new method for compiling schizophrenic synchronous programs. In International Conference on Compilers, Architecture, and Synthesis for Embedded Systems (CASES), pages 49\u201358, Atlanta, USA, November 2001. ACM.","DOI":"10.1145\/502217.502226"},{"key":"21_CR31","doi-asserted-by":"crossref","unstructured":"T. Shiple, G. Berry, and H. Touati. Constructive analysis of cyclic circuits. In European Design and Test Conference (EDTC), Paris, France, 1996. IEEE Computer Society Press.","DOI":"10.1109\/EDTC.1996.494321"},{"key":"21_CR32","unstructured":"S. Tini. Structural Operational Semantics for Synchronous Languages. PhD thesis, University of Pisa, 2000."},{"key":"21_CR33","series-title":"Lect Notes Comput Sci","first-page":"29","volume-title":"Higher Order Logic Theorem Proving and its Applications","author":"C. Zhang","year":"1993","unstructured":"C. Zhang, R. Shaw, R. Olsson, K. Levitt, M. Archer, M. Heckman, and G. Benson. Mechanizing a programming logic for the concurrent programming language microSR in HOL. In J. Joyce and C.-J. Seger, editors, Higher Order Logic Theorem Proving and its Applications, volume 780 of LNCS, pages 29\u201343, Vancouver, Canada, August 1993. University of British Columbia, Springer-Verlag, published 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\/3-540-45685-6_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,16]],"date-time":"2019-02-16T15:07:08Z","timestamp":1550329628000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45685-6_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540440390","9783540456858"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/3-540-45685-6_21","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}