Conference item
Relational algebraic ornaments
- Abstract:
-
Dependently typed programming is hard, because ideally dependently typed programs should share structure with their correctness proofs, but there are very few guidelines on how one can arrive at such integrated programs. McBride’s algebraic ornamentation provides a methodological advancement, by which the programmer can derive a datatype from a specification involving a fold, such that a program that constructs elements of that datatype would be correct by construction. It is thus...
Expand abstract
Actions
Authors
Bibliographic Details
- Publisher:
- ACM
- Host title:
- Dependently Typed Programming
- Publication date:
- 2013-01-01
- DOI:
Item Description
- UUID:
-
uuid:ee5794e5-6b3f-465c-adde-f656e1d87d30
- Local pid:
- cs:6569
- Deposit date:
- 2015-03-12
Terms of use
- Copyright date:
- 2013
If you are the owner of this record, you can report an update to it here: Report update to this record