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

Algebra of Programming using Dependent Types

Shin-Cheng Mu ; Ko Hsiang-Shang ; Patrik Jansson (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers) ; Institutionen för data- och informationsteknik, Datavetenskap (Chalmers))
Mathematics of Program Construction (0302-9743). Vol. 5133/2008 (2008), p. 268-283.
[Artikel, refereegranskad vetenskaplig]

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.

Nyckelord: Relational algebra, Program Verification, Program Calculation, Mathematics of Program Construction



Denna post skapades 2008-04-18. Senast ändrad 2014-09-02.
CPL Pubid: 70247

 

Läs direkt!


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


Institutioner (Chalmers)

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

Ämnesområden

Teoretisk datalogi
Datalogi
Programvaruteknik

Chalmers infrastruktur