Record icon

Record

Categorical organisation of the ornament–refinement framework

Abstract:

Dependently typed programming uses precise variants of data structures to ensure program correctness in an economical way, but designing reusable libraries for all possible variants of data structures is a difficult problem. The authors addressed the problem by extending McBride’s ornaments to a framework of ornaments and refinements to support a modular structure for dependently typed libraries. We use lightweight category theory to organise the ornament–refinement frame...

Expand abstract

Actions


Access Document


Files:

Authors


More by this author
Institution:
University of Oxford
Division:
MPLS
Department:
Computer Science
Role:
Author
Publisher:
Submitted to POPL'14
Publication date:
2013-07-01
UUID:
uuid:91225d69-eaf8-436d-afb7-b898eee3c6ef
Local pid:
cs:6978
Deposit date:
2015-03-04

Terms of use


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