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.
| Identifer | oai:union.ndltd.org:uiowa.edu/oai:ir.uiowa.edu:etd-5471 |
| Date | 01 December 2014 |
| Creators | Berman, Benjamin Alexander |
| Contributors | Hourcade, Juan Pablo |
| Publisher | University of Iowa |
| Source Sets | University of Iowa |
| Language | English |
| Detected Language | English |
| Type | dissertation |
| Format | application/pdf |
| Source | Theses and Dissertations |
| Rights | Copyright 2014 Benjamin Alexander Berman |
Page generated in 0.002 seconds