Machine Instruction Syntax and Semantics in Higher Order Logic

1. Necula, G.: Proof Carrying Code. In: The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, New York, pp. 106–119. ACM Press, New York (1997)

   Chapter  Google Scholar 

2. Necula, G.C.: Compiling with Proofs. PhD thesis, School of Computer Science. Carnegie Mellon University, Pittsburgh, PA (September 1998)

   Google Scholar 

3. Pfenning, F.: Logic Programming in the LF logical framework. In: Gérard, Plotkin, G. (eds.) Logical Frameworks, pp. 149–181. Cambridge University Press, Cambridge (1991)

   Chapter  Google Scholar 

4. Pfenning, F., Schürmann, C.: System description: Twelf - a meta-logical framework for deductive systems. In: The 16th International Conference on Automated Deduction, Springer, Heidelberg (1999)

   Google Scholar 

5. Appel, A., Felty, A.: A Semantic Model For Types and Machine Instructions for Proof-Carrying Code. In: The 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2000 (January 2000)

   Google Scholar 

6. Wahbe, R., Lucco, S., Anderson, T., Graham, S.: Efficient software-based fault isolation. In: Proc. 14th ACM Symposium on Operating System Principles, New York, pp. 203–216. ACM Press, New York (1993)

   Google Scholar 

7. Lindholm, T., Yellin, F.: The Java Virtual Machine Specification. Addison Wesley, Reading (1997)

   Google Scholar 

8. Ramsey, N., Fernandez, M.: The New Jersey Machine-Code Toolkit. In: Proceedings of the 1995 USENIX Technical Conference, New Orleans, LA, Han, pp. 289–302 (1995)

   Google Scholar 

9. Ramsey, N., Fernandez, M.: Specifying Representations of Machine Instructions. ACM Transactions on Programming Languages and Systems 19(3), 492–524 (1997)

   Article  Google Scholar 

10. SPARC International, Inc. The SPARC Architecture Manual v. 8. Prentice-Hall, Inc. (1992)

    Google Scholar 

11. Coquand, T., Huet, G.: The calculus of constructions. Information and Computation 76(2/3), 95–120 (1988)

    Article  MATH  MathSciNet  Google Scholar 

12. Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, Cambridge (1993)

    MATH  Google Scholar 

13. Milner, R., Weyhrauch, R.: Proving Compiler Correctness in a Mechanized Logic. Machine Intelligence 7, 51–70 (1972)

    MATH  Google Scholar 

14. Boyer, R.S., Yu, Y.: Automated Correctness Proofs of Machine Code Programs for a Commercial Microprocessor. In: The 11th International Conference of Automated Deduction, pp. 416–430. Springer, Heidelberg (1992)

    Google Scholar 

15. Wahab, M.: Verification and Abstraction of Flow-Graph Programs with Pointers and Computed Jumps. Technical Report. University of Warwick, Coventry, UK

    Google Scholar 

16. Gordon, M.: A Mechanized Hoare Logic of State Transitions. In: Roscoe, A.W. (ed.) A Classical Mind: Essays in Honour of C. A. R. Hoare, pp. 143–159. Prentice-Hall, Englewood Cliffs (1994)

    Google Scholar 

17. Gordon, M.: Mechanizing Programming Logics in Higher Order Logic. In: Birtwistle, G., Subrahmanyam, P.A. (eds.) Current Trends in Hardware Verification and Automated Theorem Proving, pp. 387–439. Springer, Heidelberg (1989)

    Google Scholar 

18. Stringer-Calvert, D.W.J.: Mechanical Verification of Compiler Correctness. Ph.D. thesis, University of York (1998)

    Google Scholar 

19. Boyer, R.S., Moore, J.S.: A Computational Logic Handbook. Academic Press, London (1988)

    MATH  Google Scholar 

Download references