Conference item icon

Conference item

Algebra of Programming using Dependent Types

Abstract:
Dependent type theory is rich enough to express that a program satisfies an input/output relational specification, but it could be hard to construct the proof term. On the other hand, squiggolists know very well how to show that one relation is included in another by algebraic reasoning. We demonstrate how to encode functional and relational derivations in a dependently typed programming language. A program is coupled with an algebraic derivation from a specification, whose correctness is guaranteed by the type system.

Actions


Access Document


Authors


Shin−Cheng Mu More by this author
Hsiang−Shang Ko More by this author
Patrik Jansson More by this author
Publisher:
Springer−Verlag
Volume:
5133
Publication date:
2008
DOI:
URN:
uuid:7e58b28b-3f4e-4c7a-baae-b0f02f17ab40
Local pid:
cs:5007

Terms of use


Metrics



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

TO TOP