Conference item icon

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


Access Document


Files:
Publisher copy:
10.1145/2502409.2502413

Authors


More by this author
Institution:
University of Oxford
Department:
Mathematical, Physical and Life Sciences Division - Department of Computer Science
Role:
Author
Publisher:
ACM
Publication date:
2013-01-01
DOI:
URN:
uuid:ee5794e5-6b3f-465c-adde-f656e1d87d30
Local pid:
cs:6569

Terms of use


Metrics


Views and Downloads






If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP