Formalizing Dijkstra

John Harrison.

Proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics, TPHOLs'98, Springer LNCS 1497, pp. 171-188.

Abstract:

We present a HOL formalization of the foundational parts of Dijkstra's classic monograph "A Discipline of Programming". While embedding programming language semantics in theorem provers is hardly new, this particular undertaking raises several interesting questions, and perhaps makes an interesting supplement to the monograph. Moreover, the failure of HOL's first order proof tactic to prove one `theorem' indicates a technical error in the book.

DVI or PostScript or PDF

Bibtex entry:

@INPROCEEDINGS{harrison-dijkstra,
        crossref        = "hol98",
        author          = "John Harrison",
        title           = "Formalizing {D}ijkstra",
        pages           = "171--188"}

@PROCEEDINGS{hol98,
        editor          = "Jim Grundy and Malcolm Newey",
        booktitle       = "Theorem Proving in Higher Order Logics:
                           11th International Conference, TPHOLs'98",
        series          = "Lecture Notes in Computer Science",
        volume          = 1497,
        address         = "Canberra, Australia",
        date            = "September/October 1998",
        year            = 1998,
        publisher       = "Springer-Verlag"}