Document Type

Dissertation

Date of Degree

Fall 2014

Degree Name

PhD (Doctor of Philosophy)

Degree In

Computer Science

First Advisor

Juan Pablo Hourcade

Abstract

Interactive theorem provers are software tools that help users create machine-checked proofs. Although difficult to use, they have been playing an important role in the effort to create highly reliable software. I present several novel user interface ideas for interactive theorem provers, generalizable to other mathematics and programming tools. Prototypes tailored to the Coq interactive theorem prover were developed and tested in an experiment with human participants. The results show promising directions for making interactive theorem provers easier to use.

Public Abstract

This dissertation discusses the development and testing, with human participants, of several novel user interfaces for interactive theorem provers. Interactive theorem provers are software tools used to precisely describe and correctly reason about mathematical ideas and, in particular, to create and check what are often very complex mathematical proofs. One important application is the development of proofs about software so as to ensure higher levels of reliability in critical (e.g. aviation, automotive, financial, medical) software than are possible with software testing alone. Improved user interfaces for interactive theorem provers are important for allowing more widespread, efficient, and effective use of these tools. In addition, most of the user interface ideas generated in the context of interactive theorem provers can be generalized for use with other applications, especially programming environments, and present new directions for human-computer interaction more broadly.

Keywords

publicabstract, Interactive Theorem Provers, User Interfaces

Pages

xi, 152 pages

Bibliography

Includes bibliographical references (pages 144-152).

Copyright

Copyright 2014 Benjamin Alexander Berman

Share

COinS