Rewriting of imperative programs into logical equations

Antoy, 1994, Using term rewriting to verify software, IEEE Transactions on Software Engineering, 20, 259, 10.1109/32.277574 Baader, 1998 B. Barras, S. Boutin, C. Cornes, J. Courant, J. Filliâtre, E. Giménez, H. Herbelin, G. Huet, C. Munoz, C. Murthy, C. Parent, C. Paulin, A. Saïbi, B. Werner, The coq proof assistant reference manual–Version V6.1, Tech. Rep. 0203, INRIA, August 1997 Bergstra, 1997, Toward a complete transformational toolkit for compilers, ACM Transactions on Programming Languages and Systems, 19, 639, 10.1145/265943.265944 Bouhoula, 1992, Spike: An automatic theorem prover, vol. 624, 460 F.Q. da Silva, On observational equivalence and compiler correctness, in: Proc. Internat. Conf. on Computing and Information (ICCI), 1994, pp. 17–34 C. Fédèle, E. Kounalis, Automatic proofs of properties of simple C−− modules, in: Proc. 14th IEEE Internat. Conf. on Automated Software Engineering, Cocoa Beach, FL, 1999, pp. 283–286 Field, 1998, Equations as a uniform framework for partial evaluation and abstract interpretation, ACM Computing Surveys, 30, 2, 10.1145/289121.289123 Filliâtre, 1998, Proof of imperative programs in type theory, vol. 1657, 78 S. Garland, J. Guttag, A guide to LP, the Larch Prover, Tech. Rep. 82, Digital Equipment Corporation, Systems Research Centre, December, 1991 Gibbons, 1998, Declarative view of imperative programs Goguen, 1996, Algebraic semantics of imperative programs Hoare, 1969, An axiomatic basis for computer programming, Communications of the ACM, 12, 576, 10.1145/363235.363259 Jacobs, 2003, Coalgebras and monads in the semantics of Java, Theoretical Computer Science, 291, 329, 10.1016/S0304-3975(02)00366-3 Juellig, 1996, SPECWARE: An advanced environment for the formal development of complex software systems, Lecture Notes in Computer Science, 1101, 551, 10.1007/BFb0014339 Kapur, 1988, RRL: a rewrite rule laboratory, vol. 310, 768 Knuth, 1970, Simple word problems in universal algebras, 263 Milner, 1979, LCF: A way of doing proofs with a machine, vol. 74, 146 Moggi, 1991, Notions of computation and monads, Information and Computation, 93, 55, 10.1016/0890-5401(91)90052-4 Owre, 1992, PVS: A prototype verification system, vol. 607, 748 O. Ponsini, C. Fédèle, E. Kounalis, SOS C−−: A system for interpreting operational semantics of C−− programs, in: M.H. Hamza (Ed.), Proc. IASTED Internat. Conf. on Applied Informatics, Innsbruck, Austria, 2002, pp. 164–169 Schweizer, 1997, Verifying the specification-to-code correspondence for abstract data types, vol. 11 Scott, 1971, Towards a mathematical semantics for computer languages, 19 Traynor, 1997, The Cogito development system, vol. 1349, 586 Wadler, 1998, The marriage of effects and monads, 63 Ward, 1993, Abstracting a specification from code, Journal of Software Maintenance: Research and Practice, 5, 101, 10.1002/smr.4360050204