Journal article icon

Journal article

Modularising inductive families

Abstract:

Dependently typed programmers are encouraged to use inductive families to integrate constraints with data construction. Different constraints are used in different contexts, leading to different versions of datatypes for the same data structure. For example, sequences might be constrained by length or by an ordering on elements, giving rise to different datatypes “vectors” and “sorted lists” for the same underlying data structure of sequences. Modular implementation of common operations fo...

Expand abstract

Actions


Access Document


Files:
Publisher copy:
10.2201/NiiPi.2013.10.5

Authors


More by this author
Institution:
University of Oxford
Division:
MPLS
Department:
Computer Science
Role:
Author
Journal:
Progress in Informatics More from this journal
Issue:
10
Pages:
65-88
Publication date:
2013-01-01
DOI:
UUID:
uuid:2243c8af-07d5-42f4-b7d4-8ccf7451c281
Local pid:
cs:6002
Deposit date:
2015-03-12

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