Compilation and Synthesis for Real-Time Embedded Controllers - Correct System Design: Recent Insights and Advances - page 276

18. N. Halbwachs. Synchronous Programming of Reactive Systems . Kluwer, 1993.
19. He Jifeng, I. Page, and J. P. Bowen. Towards a provably correct hardware im-
plementation of Occam. In G. J. Milne and L. Pierre, editors, Correct Hardware
Design and Verication Methods , LNCS 683, pages 214{225. Springer-Verlag, 1993.
20. C. A. R. Hoare. Renement algebra proves correctness of compiling specica-
tions. In C. C. Morgan and J. C. P. Woodcock, editors, 3rd Renement Workshop ,
Workshops in Computer Science, pages 33{48. Springer-Verlag, 1991.
21. C. A. R. Hoare, I. J. Hayes, He Jifeng, C. C. Morgan, A. W. Roscoe, J. W. Sanders,
I. H. Sorenson, J. M. Spivey, and B. A. Sufrin. Laws of programming. Communi-

cations of the ACM , 30(8):672{687, 1987.
22. C. A. R. Hoare, He Jifeng, and A. Sampaio. Normal form approach to compiler
design. Acta Informatica , 30:701{739, 1993.
23. inmos limited. Transputer Instruction Set { A Compiler Writer's Guide . Prentice
Hall International, rst edition, 1988.
24. J. J. Joyce. Totally veried systems: Linking veried software to veried hardware.
In Leeser and Brown [25], pages 177{201.
25. M. Leeser and G. Brown, editors. Hardware Specication, Verication and Syn-
thesis: Mathematical Aspects , LNCS 408, Springer-Verlag, 1990.
26. O. Maler, A. Pnueli, and J. Sifakis. On the synthesis of discrete controllers for
timed systems. In Meyer and Puech [29], pages 229{242.
27. A. J. Martin. The design of a delay-insensitive microprocessor: An example of
circuit synthesis by program transformation. In Leeser and Brown [25], pages

244{259.
28. J. McCarthy and J. Painter. Correctness of a compiler for arithmetic expressions.
In J. Schwarz, editor, Proc. Symp. Applied Mathematics , pages 33{41. American
Mathematical Society, 1967.
29. E. W. Meyer and C. Puech, editors. Symposium on Theoretical Aspects of Computer
Science (STACS 95) , LNCS 900, Springer-Verlag, 1995.
30. R. Milner, M. Tofte, and R. Harper. The Denition of Standard ML .TheMIT

Press, 1990.
31. J S. Moore. Piton, A Mechanically Veried Assembly-Level Language .Kluwer
Academic Publishers, 1996.
32. C. Morgan and T. Vickers (Eds.). On the Renement Calculus . Springer-Verlag,

1994.
33. F. L. Morris. Advice on structuring compilers and proving them correct. In Pro-
ceedings ACM Symposium on Principles of Programming Languages (PoPL'93) ,
pages 144{152, 1973.
34. J. M. Morris. A theoretical basis for stepwise renement and the programming
calculus. Science of Computer Programming , 9:287{306, 1987.
35. J. M. Morris. Laws of data renement. Acta Informatica , 26:287{308, 1989.
36. M. Muller-Olm. A short description of the prototype compiler. ProCoS Technical
Report Kiel MMO 14/1, Christian-Albrechts-Universitat Kiel, Germany, August
1995.
37. M. Muller-Olm. Modular Compiler Verication: A Process-Algebraic Approach
Advocating Stepwise Abstraction , LNCS 1283, Springer-Verlag, 1997.
38. T. S. Norvell. Machine code programs are predicates too. In D. Till, editor,
6th Renement Workshop , Workshops in Computing. Springer-Verlag and British
Computer Society, 1994.
39. D. J. Pavey and L. A. Winsborrow. Demonstrating equivalence of source code and
PROM contents. The Computer Journal , 36(7):654{667, 1993.