[High Integrity Compilation] Susan Stepney.
High Integrity Compilation : a case study .

Prentice-Hall, 1993.

A. Bibliography

[Abramson and Dahl 1989]
Harvey Abramson and Veronica Dahl. Logic Grammars . Symbolic Computation series. Springer Verlag, 1989.

[Aho and Ullman 1977]
Alfred V. Aho and Jeffrey D. Ullman. Principles of Compiler Design . Addison-Wesley, 1977.

[Aho et al. 1988]
Alfred V. Aho, Brian W. Kernighan, and Peter J. Weinberger. The AWK Programming Language . Addison-Wesley, 1988.

[Allison 1986]
L. Allison. A Practical Introduction to Denotational Semantics . Cambridge University Press, 1986.

[Andrews et al. 1991]
Derek J. Andrews, Don Ward, Roger Henry, et al. CD10514-2(draft):1991 fourth working draft Modula-2 standard, 1991.

[Austin 1976]
J. L. Austin. How to do Things with Words . Oxford University Press, 2nd edition, 1976.

[Bergeretti and Carré 1985]
J. F. Bergeretti and B. Carré. Information flow and data flow analysis of while programs. ACM Transactions on Programming Languages and Systems , 7:37--61, 1985.

[Bramson 1984]
B. D. Bramson. Malvern's program analysers. RSRE Research Review , 1984.

[Carré 1989]
Bernard A. Carré. Reliable programming in standard languages. In Chris T. Sennett, editor. High-integrity Software . Pitman, 1989.

[Clocksin and Mellish 1987]
W. F. Clocksin and C. S. Mellish. Programming in Prolog . Springer Verlag, 3rd edition, 1987.

[Cohn 1979]
Avra J. Cohn. Machine Assisted Proofs of Recursion Implementation . PhD thesis, University of Edinburgh, 1979.

[Cousot and Cousot 1977]
Patrick Cousot and Radhia Cousot. Abstract interpretation: a unified lattice model for static ana lysis of programs by construction or approximation of fixed points. In Proceedings of the Fourth Annual ACM Symposium on the Principles of Programming Languages . ACM, 1977.

[De Millo et al. 1979]
R. A. De Millo, R. J. Lipton, and A. J. Perlis. Social processes and proofs of theorems and programs. Communications of the ACM , 22(5):271--280, 1979. see also 'ACM Forum', 22(11):621--630.

[Gordon 1979]
Michael J. C. Gordon . The Denotational Description of Programming Languages---An Introduction . Springer Verlag, 1979.

[Hall 1990]
J. Anthony Hall . Seven myths of formal methods. IEEE Software , pages 21--28, September 1990.

[Hayes 1987]
Ian Hayes. Specification Case Studies . Prentice Hall, 1987.

[Hoare 1991]
C. A. R. Hoare . Refinement algebra proves correctness of compiling specifications. In C. Carroll Morgan and James C. P. Woodcock, editors, 3rd BCS-FACS Refinement Workshop , Workshops in Computing, pp 33--48. Springer-Verlag, 1991.

[Hoare and Jones 1989]
C. A. R. Hoare and Cliff B. Jones. Essays in Computer Science . Prentice Hall, 1989.

[Kernighan and Pike 1984]
Brian W. Kernighan and Rob Pike. The Unix Programming Environment . Prentice Hall, 1984.

[Knuth 1968]
Donald E. Knuth . Semantics of context-free languages. Mathematical Systems Theory , 2(2):127--145, 1968. correction, 5(1):95--96, 1971.

[Lee 1989]
Peter Lee. Realistic Compiler Generation . Foundations of Computing series. MIT Press, 1989.

[McCarthy and Painter 1966]
J. McCarthy and J. Painter. Correctness of a compiler for arithmetic expressions. Technical Report AIM-40, Stanford University, 1966.

[Meyer 1985]
Bertrand Meyer. On formalism in specifications . IEEE Software , 2:6--26, January 1985.

[Meyer 1990]
Bertrand Meyer. Introduction to the Theory of Programming Languages . Prentice Hall, 1990.

[Milner and Weyhrauch 1972]
Robin Milner and R. Weyhrauch. Proving compiler correctness in a mechanized logic. Machine Intelligence , 7, 1972.

[Morris 1973]
F. L. Morris. Advice on structuring compilers and proving them correct. In Proceedings of the First Annual ACM Symposium on Principles of Programming Languages , pages 144--152. ACM, 1973.

[Mosses 1975]
Peter D. Mosses. Mathematical Semantics and Compiler Generation . PhD thesis, University of Oxford, 1975.

[Neumann 1985]
Peter G. Neumann. Some computer-related disasters and other egregious horrors. ACM SIGSOFT Software Engineering Notes , 10(1):6, 1985.

[Parker 1991]
Colin E. Parker. Z tools catalogue. ZIP document ZIP/BAe/90/020, British Aerospace, Warton, May 1991.

[Paulson 1981]
L. Paulson . A Compiler Generator for Semantic Grammars . PhD thesis, Stanford University, 1981.

[Paulson 1982]
L. Paulson . A semantics-directed compiler generator. In Proceedings of the Ninth Annual ACM Symposium on Principles of Programming Languages , pages 224--239. ACM, 1982.

[Polak 1981]
Wolfgang Polak. Compiler Specification and Verification , volume 124 of Lecture Notes in Computer Science . Springer Verlag, 1981.

[Potter et al. 1991]
Ben Potter, Jane Sinclair, and David Till . An Introduction to Formal Specification and Z . Prentice Hall, 1991.

[Schmidt 1988]
David A. Schmidt. Denotational Semantics: A Methodology for Language Development . Wm. C. Brown Publishers, 1988.

[Spivey 1992]
J. Michael Spivey. The Z Notation: a Reference Manual . Prentice Hall, 2nd edition, 1992.

[Stepney and Lord 1987]
Susan Stepney and Stephen P. Lord. Formal specification of an access control system . Software---Practice and Experience , 17(9):575--593, 1987.

[Stepney et al. 1991]
Susan Stepney , Dave Whitley, David Cooper, and Colin Grant. A demonstrably correct compiler . BCS Formal Aspects of Computing , 3:58--101, 1991.

[Sterling and Shapiro 1986]
Leon Sterling and Ehud Shapiro. The Art of Prolog: Advanced Programming Techniques . MIT Press, 1986.

[Stoy 1977]
Joseph E. Stoy. Denotational Semantics and the Scott-Strachey Approach to Programming Language Theory . MIT Press, 1977.

[Tennent 1991]
R. D. Tennent. Semantics of Programming Languages . Prentice Hall, 1991.

[Tofte 1990]
Mads Tofte. Compiler Generators: what they can do, what they might do, and what they will probably never do , volume 19 of EATCS Monographs on Theoretical Computer Science . Springer Verlag, 1990.

[Wand 1984]
M. Wand. A semantic prototyping system. Proceedings of the SIGPLAN 84 Symposium on Compiler Construction; ACM SIGPLAN Notices , 19(6):213--221, 1984.

[Warren 1980]
David H. Warren. Logic programming and compiler writing. Software---Practice and Experience , 10:97--125, 1980.

[Woodcock and Brien 1992]
James C. P. Woodcock and Stephen M. Brien. W: A logic for Z . In John E. Nicholls, editor. Proceedings of the 6th Annual Z User Meeting, York 1991 , Workshops in Computing. Springer Verlag, 1992.