FP /
AoPAgda
Algebra of Programming in Agda
Shin-Cheng Mu, Josh Ko and Patrik Jansson wrote first a conference paper (MPC 2008) and later an extended journal paper (JFP 2009) with accompanying Agda code.
There is ongoing work (2012-2014) in the Strongly Typed Libraries for Programs and Proofs project including an application to the Algebra of Parallel Programming in Agda and Valiant Agda.
Journal paper bib entry
@Article{MuKoJansson2009AoPA, author = {Shin-Cheng Mu and Hsiang-Shang Ko and Patrik Jansson}, title = {Algebra of programming in {Agda}: dependent types for relational program derivation}, publisher = {Cambridge University Press}, journal = {Journal of Functional Programming}, volume = 19, issue = 5, pages = {545--579}, year = 2009, doi = "10.1017/S0956796809007345", fulltext = "http://www.iis.sinica.edu.tw/~scm/pub/aopa.pdf" }
Conference paper bib entry
@InProceedings{mukojansson08:mpc:dcc, author = {Shin-Cheng Mu and Hsiang-Shang Ko and Patrik Jansson}, title = {Algebra of Programming using Dependent Types}, booktitle = {Mathematics of Program Construction}, year = 2008, series = "LNCS", publisher = "Springer", volume = "5133/2008", pages = "268--283", doi = "10.1007/978-3-540-70594-9_15" }