Book chapter
The Design of a Practical Proof Checker for a Lazy Functional Language
Trends in Functional Programming, pp.117-132
Lecture Notes in Computer Science, Springer Berlin Heidelberg
2013
DOI: 10.1007/978-3-642-40447-4_8
Abstract
Pure, lazy functional languages like Haskell provide a sound basis for formal reasoning about programs in an equational style. In practice, however, equational reasoning about correctness proofs is underutilized. In the context of Haskell, we suggest that part of the reason for this is the lack of accessible tools for machine-checked equational reasoning. This paper outlines the design of MProver, a proof checker which fills just that niche. MProver features first-class support for reasoning about potentially undefined computations (particularly important in a lazy setting), and an extended notion of Haskell-like type classes, enabling a highly modular style of program verification that closely follows familiar functional programming idioms.
Details
- Title: Subtitle
- The Design of a Practical Proof Checker for a Lazy Functional Language
- Creators
- Adam Procter - University of MissouriWilliam L. Harrison - University of MissouriAaron Stump - University of Iowa
- Resource Type
- Book chapter
- Publication Details
- Trends in Functional Programming, pp.117-132
- Publisher
- Springer Berlin Heidelberg; Berlin, Heidelberg
- Series
- Lecture Notes in Computer Science
- DOI
- 10.1007/978-3-642-40447-4_8
- eISSN
- 1611-3349
- ISSN
- 0302-9743
- Language
- English
- Date published
- 2013
- Academic Unit
- Computer Science
- Record Identifier
- 9984259500202771
Metrics
3 Record Views