Jim Grundy's Research Interests

The basic motivation that drives my research is a desire to be able to construct formally verified computer systems. I am liable to take an interest in anything that would help me in that goal. Having said that, there are three areas within this field in which I maintain a particular interest: interactive mechanised reasoning, program refinement, and proof presentation. Below you can find a description of these areas and a list of my publications relating to them. There is some overlap here, so the same publication may appear under various headings.

More information about the publications below is available via my publications page.

Interactive Mechanised Reasoning

Mechanised, interactive, reasoning; novel interactive proof forms; effective mechanised support for human style reasoning.

Publications

• Jim Grundy and Malcolm Newey, editors. Theorem Proving in Higher Order Logics: 11th International Conference, TPHOLs'98, volume 1479 of Lecture Notes in Computer Science, Canberra, Australia, September/October 1998. Springer-Verlag.
• Jim Grundy and Malcolm Newey, editors. Theorem Proving in Higher Order Logics: Emerging Trends - Supplementary Proceedings of the 11th International Conference, TPHOLs'98, Joint Computer Science Technical Report TR-CS-98-08, Canberra, Australia, September/October 1998. The Australian National University, Department of Computer Science, Canberra ACT 0200, Australia.
• Michael Butler, Jim Grundy, Thomas Långbacka, Rimvydas Ruksenas & Joakim von Wright. The Refinement Calculator: Proof Support for Program Refinement. In Groves & Reeves, eds. Formal Methods Pacific'97: Proceedings of FMP'97, Discrete Mathematics and Theoretical Computer Science Series., July 1997, Wellington. Springer-Verlag, Singapore. pages 40-61.
• Joakim von Wright, Jim Grundy and John Harrison, editors. Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs'96, volume 1125 of Lecture Notes in Computer Science, Turku, Finalnd, August 1996. Springer-Verlag.
• Joakim von Wright, Jim Grundy and John Harrison, editors. Supplementary Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics: TPHOLs'96, number 1 in TUCS General Publications, Turku, Finland, August 1996. Turku Centre for Computer Science, Lemminkäisenkatu 14A, 20520 Turku, Finland.
• Jim Grundy. Transformational hierarchical reasoning. The Computer Journal. 39(4):291-302. May 1996.
• Jim Grundy and Thomas Långbacka. Towards a Browsable Record of HOL Proofs. Technical Report 7. Turku Centre for Computer Science, Lemminkäisenkatu 14A, 20520 Turku, Finland. April 1996.
• Jim Grundy. Trustworthy Storage and Exchange of Theorems. Technical Report 1. Turku Centre for Computer Science, Lemminkäisenkatu 14A, 20520 Turku, Finland. April 1996.
• Jim Grundy. A Window Inference Tool for Refinement. In Jones, et.al. (eds). Proceedings of the 5th Refinement Workshop, Workshops in Computing. January 1992, London. Springer-Verlag, London. pages 230-254.
• Jim Grundy. Window Inference in the HOL System. In Archer, et.al. (eds). Proceedings of the International Workshop on the HOL Theorem Proving System and Its Applications. August 1991, Davis. IEEE Computer Society Press, Los Alamitos. pages 177-189.
• Jim Grundy. Report on m-EVES. Research Report ERL-0545-RR. Electronics & Surveillance Research Laboratory, PO Box 1500, Salisbury SA 5108, Australia. March 1991.

Program Refinement

Program refinement: the step-wise, formal derivation of programs from their specifications; weakest precondition semantics and its representation in higher order logics; predicative programming semantics.

Publications

• Jim Grundy, Martin Schwenke and Trevor Vickers, editors. International Refinement Workshop and Formal Methods Pacific 1998. In Discrete Mathematics and Theoretical Computer Science, Canberra, Australia, September/October 1998. Springer-Verlag.
• Jim Grundy, Martin Schwenke and Trevor Vickers, editors. Supplementary proceedings of the International Refinement Workshop and Formal Methods Pacific 1998. Joint Computer Science Technical Report TR-CS-98-09. The Australian National University, Department of Computer Science, Canberra ACT 0200, Australia. September 1996.
• Michael Butler, Jim Grundy, Thomas Långbacka, Rimvydas Ruksenas & Joakim von Wright. The Refinement Calculator: Proof Support for Program Refinement. In Groves & Reeves, eds. Formal Methods Pacific'97: Proceedings of FMP'97, Discrete Mathematics and Theoretical Computer Science Series., July 1997, Wellington. Springer-Verlag, Singapore. pages 40-61.
• Jim Grundy. A Method of Program Refinement. PhD Thesis, Technical Report 318. University of Cambridge, Computer Laboratory, New Museums Site, Pembroke Street, Cambridge CB2 3QG, England. November 1993.
• Jim Grundy. Predicative Programming - A Survey. In Bjørner, et.al. (eds). Formal Methods in Programming and Their Applications: Proceedings of the International Conference, volume 735 of Lecture Notes in Computer Science. Novosibirsk, Russia, June 1993. Springer-Verlag. pages 8-25.
• Jim Grundy. A Three-Valued Logic for Refinement. In Bjørner, et.al. (eds). Formal Methods in Programming and Their Applications: Proceedings of the International Conference, volume 735 of Lecture Notes in Computer Science. Novosibirsk, Russia, June 1993. Springer-Verlag. pages 26-42.
• Jim Grundy. A Window Inference Tool for Refinement. In Jones, et.al. (eds). Proceedings of the 5th Refinement Workshop, Workshops in Computing. January 1992, London. Springer-Verlag, London. pages 230-254.

Proof Presentation

The presentation of formal, machine checkable, proofs for easy reading by humans.

Publications

• Ralph Back, Jim Grundy, and Joakim von Wright. Structured Calculational Proof. Formal Aspects of Computing. 9(5-6):469-483. 1997.

   

  Ralph Back, Jim Grundy and Joakim von Wright. Structured Calculational Proof. Joint Computer Science Technical Report TR-CS-96-09. The Australian National University, Department of Computer Science, Canberra ACT 0200, Australia. November 1996.

   

  Ralph Back, Jim Grundy and Joakim von Wright. Structured Calculational Proof. TUCS Technical Report 65. Turku Centre for Computer Science, Lemminkäisenkatu 14A, 20520 Turku, Finland. November 1996.
• Jim Grundy and Thomas Långbacka. Recording HOL Proofs in a Structured Browsable Format. In Johnson (ed). Algebraic Methodology and Software Technology: Proceedings of the 6th International Conference, AMAST'97, volume 1349 of Lecture Notes in Commputer Science, Sydney, December 1997. Springer-Verlag. pages 567-571.
• Jim Grundy. A browsable format for proof presentation. Mathesis Universalis, 1(2), Spring 1996.

   

  Jim Grundy. A Browsable Format for Proof Presentation. In Gefwert, et.al. (eds). Logic, Mathematics and the Computer - Foundations: History, Philosophy and Applications, volume 14 of Symposium Series. June 1996, Helsinki. Finnish Artificial Intelligence Society. pages 171-178.
• Jim Grundy and Thomas Långbacka. Towards a Browsable Record of HOL Proofs. Technical Report 7. Turku Centre for Computer Science, Lemminkäisenkatu 14A, 20520 Turku, Finland. April 1996.