Proof Style

John Harrison.

Proceedings of the BRA TYPES'96 workshop on Types for Proofs and Programs (Aussois), Springer LNCS 1512, pp. 154-172, 1996.

Abstract:

We are concerned with how computer theorem provers should expect users to communicate proofs to them. There are many stylistic choices that still allow the machine to generate a completely formal proof object. The most obvious choice is the amount of guidance required from the user, or from the machine perspective, the degree of automation provided. But another important consideration, which we consider particularly significant, is the bias towards a `procedural' or `declarative' proof style. We will explore this choice in depth, and discuss the strengths and weaknesses of declarative and procedural styles for proofs in pure mathematics and for verification applications. We conclude with a brief summary of our own experiments in trying to combine both approaches.

DVI or Postscript or PDF

Bibtex entry:

@INPROCEEDINGS{harrison-style,
        crossref        = "types96",
        author          = "John Harrison",
        title           = "Proof Style",
        pages           = "154--172"}

@PROCEEDINGS{types96,
        editor          = "Eduardo Gim{\'e}nex and Christine Pausin-Mohring",
        booktitle       = "Types for Proofs and Programs: International
                           Workshop {TYPES'96}",
        series          = "Lecture Notes in Computer Science",
        volume          = 1512,
        address         = "Aussois, France",
        date            = "15--19 September 1996",
        year            = 1996,
        publisher       = "Springer-Verlag"}