[Agda] AoPA -- Algebra of Programming in Agda (updated 2016)

[Shin-Cheng Mu]

Hi all,

This is a notification that the library Algebra of Programming
in Agda (AoPA) has been updated and now works with Agda 2.5.1.

AoPA allows one to encode Algebra of Programming (BdM97) style 
program derivation, both functional and relational, in Agda.

New additions include the use of universe polymorphism, 
generic datatypes with polymorphic base functors, and theories 
for developing algorithms from Galois connections (MO11, CM15). 

Development of AoPA is still being continued. For more info,
see the Git Repository:

  https://github.com/scmu/aopa

====

The program derivation community has been exploring a relational 
theory of program calculation. A problem is specified as a relation 
that maps inputs to outputs, which allows us not to be over 
specific about which output to choose when they are equally good, 
leaving the choices to implementations. The task is to refine the 
specification into a functional implementation, using algebraic 
properties.

AoPA allows us to to develop relational proofs, in Agda, in the 
style of Bird and de Moor. Elements of the relational theory of 
programs are modelled in the type system of Agda. Calculations 
are expressed as program terms that, if type-checked, is guaranteed 
to be correct. In the end of a calculation one may extract a 
functional program that is proved to respect the relational 
specification.

sincerely, 
Shin
scm at iis.sinica.edu.tw

(BdM97) Richard Bird and Oege de Moor, Algebra of Programming. 
Prentice Hall, 1997.

(MO11) Shin-Cheng Mu and José Nuno Oliveira, Programming from 
Galois connections. The Journal of Logic and Algebraic Programming, 
Volume 81, Issue 6, August 2012, pp 680–704. doi>10.1016/j.jlap.2012.05.003.

(CM15) Yu-Hsi Chiang and Shin-Cheng Mu, Formal derivation of 
greedy algorithms from relational specifications: A tutorial. 
Journal of Logical and Algebraic Methods in Programming. In Press.