CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Algebra of programming in Agda: dependent types for relational program derivation

Shin-Cheng Mu ; Hsiang-Shang Ko ; Patrik Jansson (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers))
Journal of Functional Programming (0956-7968). Vol. 19 (2009), 5, p. 545 - 579.
[Artikel, refereegranskad vetenskaplig]

Relational program derivation is the technique of stepwise refining a relational specification to a program by algebraic rules. The program thus obtained is correct by construction. Meanwhile, dependent type theory is rich enough to express various correctness properties to be verified by the type checker. We have developed a library, AoPA (Algebra of Programming in Agda), to encode relational derivations in the dependently typed programming language Agda. A program is coupled with an algebraic derivation whose correctness is guaranteed by the type system. Two non-trivial examples are presented: an optimisation problem and a derivation of quicksort in which well-founded recursion is used to model terminating hylomorphisms in a language with inductive types.

Denna post skapades 2009-03-25. Senast ändrad 2016-08-18.
CPL Pubid: 91898


Läs direkt!

Länk till annan sajt (kan kräva inloggning)

Institutioner (Chalmers)

Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers) (2008-2010)


Teoretisk datalogi

Chalmers infrastruktur