Thesis
A Functional and Monadic Proof Assistant for Streams
- Abstract:
- Streams, which are infinite sequences of elements, are defined by a coinductive datatype and operations on streams are corecursive programs. Equations that define streams, under light restrictions, have a unique solution. This project presents the discussion and implementation of a proof assistant that supports this proof method. The tool is implemented in the purely functional language Haskell and makes extensive use of monads. The emphasis of the project is placed on simplicity, clarity and terseness.
Actions
Authors
- Publication date:
- 2008-09-01
- Type of award:
- DPhil
- Level of award:
- Doctoral
- UUID:
-
uuid:1cc82d25-9079-4877-a308-e045d0e8e436
- Local pid:
-
cs:4880
- Deposit date:
-
2015-03-31
Terms of use
- Copyright holder:
- James, D
- Copyright date:
- 2008
If you are the owner of this record, you can report an update to it here: Report update to this record