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"
  }