Dr. Shin-Cheng Mu

Institute of Information Science, Academia Sinica

Speech title: Algebra of Programming in Agda

Abstract:

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, 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.