Verification of the correctness of compiler optimization using co-induction

References

• Brzozowski , J. A. 1964 . Derivatives of regular expressions . Journal of the ACM , 11 : 481 – 494 .
   Web of Science ®Google Scholar
• Hopcroft , J. E. and Ullman , J. D. 1979 . Introduction to Automata Theory, Languages and Computation , Addison Wesley .
   Google Scholar
• Chen , H. and Pucella , R. 2003 . A co-algebraic approach to Kleene algebra with tests electronic . Notes in Theoretical Computer Science , 82 ( 1 )
   Google Scholar
• Kozen , D. 1994 . A completeness theorem for Kleene algebras and the algebra of regular events . Information and Computation , 110 : 366 – 390 .
   Web of Science ®Google Scholar
• Kozen , D. 1997 . Kleene algebra with tests . Transactions on Programming Languages and Systems , 19 : 427 – 443 .
   Web of Science ®Google Scholar
• Kozen , D. 1998 . “ Typed Kleene algebra ” . In Technical Report 98–1669 , Computer Science Department, Cornell University .
   Google Scholar
• Kozen , D. 1999 . “ On Hoare logic and Kleene algebra with tests ” . In Proceedings of the Conference on Logic in Computer Science (LICS’99) 167 – 172 . in
   Google Scholar
• Kozen , D. 2001 . “ Automata on guarded strings and applications ” . In Technical Report 2001–1833 , Computer Science Department, Cornell University .
   Google Scholar
• Kozen , D. Scope of Logic, Methodology, and Philosophy of Science . 11th International Congress Logic, Methodology and Philosophy of Science . August 1999 , Cracow . On Hoare logic, Kleene algebra and types , Vol. 1 , pp. 119 – 133 . in, of the, Studies in Epistemology, Logic, Methodology, and Philosophy of Science, 315, Kluwer
   Google Scholar
• Kozen , D. and Patron , M. C. January 1998 . “ Certification of code optimization using Kleene algebra with tests ” . In Technical Report 98–1961 , January , Computer Science Department, Cornell University .
   Google Scholar
• Rutten , J. J. M. M. 1998 . “ Automata and coinduction (an exercise in coalgebra) ” . In Proceedings of CONCUR’98 , Lecture Notes in Computer Science Vol. 1466 , 193 – 217 . in
   Google Scholar
• Rutten , J. J. M. M. 1999 . A note on coinduction and weak bisimilarity for while programs . Theoretical Informatics and Applications (RAIRO) , 33 : 393 – 400 .
   Google Scholar
• Lidl , R. and Pilz , G. 1984 . Applied Abstract Algebra , New York : Springer-Verlag .
   Google Scholar