A Functional and Monadic Proof Assistant for Streams
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...
| Main Author: | |
|---|---|
| Format: | Thesis |
| Published: |
2008
|
| _version_ | 1797112334315945984 |
|---|---|
| author | James, D |
| author_facet | James, D |
| author_sort | James, D |
| collection | OXFORD |
| description | 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. |
| first_indexed | 2024-03-07T08:24:12Z |
| format | Thesis |
| id | oxford-uuid:1cc82d25-9079-4877-a308-e045d0e8e436 |
| institution | University of Oxford |
| last_indexed | 2024-03-07T08:24:12Z |
| publishDate | 2008 |
| record_format | dspace |
| spelling | oxford-uuid:1cc82d25-9079-4877-a308-e045d0e8e4362024-02-12T11:30:13ZA Functional and Monadic Proof Assistant for StreamsThesishttp://purl.org/coar/resource_type/c_db06uuid:1cc82d25-9079-4877-a308-e045d0e8e436Department of Computer Science2008James, DStreams, 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. |
| spellingShingle | James, D A Functional and Monadic Proof Assistant for Streams |
| title | A Functional and Monadic Proof Assistant for Streams |
| title_full | A Functional and Monadic Proof Assistant for Streams |
| title_fullStr | A Functional and Monadic Proof Assistant for Streams |
| title_full_unstemmed | A Functional and Monadic Proof Assistant for Streams |
| title_short | A Functional and Monadic Proof Assistant for Streams |
| title_sort | functional and monadic proof assistant for streams |
| work_keys_str_mv | AT jamesd afunctionalandmonadicproofassistantforstreams AT jamesd functionalandmonadicproofassistantforstreams |