publications:
- title: "Algebra of Programming Using Dependent Types"
  author:
  - name: "Shin-Cheng Mu"
    link: "http://www.iis.sinica.edu.tw/~scm/"
  - name: "Hsiang-Shang Ko"
    link: "http://joshkos.blogspot.se/"
  - name: "Patrik Jansson"
    link: "http://www.chalmers.se/cse/EN/people/jansson-patrik"
  year: "2008"
  doi: "http://dx.doi.org/10.1007/978-3-540-70594-9_15"
  abstract: "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."
  links:
    doi: "http://dx.doi.org/10.1007/978-3-540-70594-9_15"
  tags:
  - "programming languages"
  - "functional programming"
  - "relational algebra"
  - "type system"
  - "algebraic specification"
  - " algebra"
  - "programming"
  - "type theory"
  researchr: "https://researchr.org/publication/MuKJ08"
  cites: 0
  citedby: 0
  pages: "268-283"
  booktitle: "mpc"
  kind: "inproceedings"
  key: "MuKJ08"
- title: "Algebra of programming in Agda: Dependent types for relational program derivation"
  author:
  - name: "Shin-Cheng Mu"
    link: "http://www.iis.sinica.edu.tw/~scm/"
  - name: "Hsiang-Shang Ko"
    link: "http://joshkos.blogspot.se/"
  - name: "Patrik Jansson"
    link: "http://www.chalmers.se/cse/EN/people/jansson-patrik"
  year: "2009"
  doi: "http://dx.doi.org/10.1017/S0956796809007345"
  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 (Algebra of Programming in Agda), 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. Two non-trivial examples are presented: an optimisation problem and a derivation of quicksort in which well-founded recursion is used to model terminating hylomorphisms in a language with inductive types."
  links:
    doi: "http://dx.doi.org/10.1017/S0956796809007345"
  tags:
  - "programming languages"
  - "rule-based"
  - "meta programming"
  - "program verification"
  - "meta-model"
  - "modeling language"
  - "language modeling"
  - "relational algebra"
  - "type system"
  - "rules"
  - "algebraic specification"
  - " algebra"
  - "programming"
  - "type theory"
  - "Meta-Environment"
  researchr: "https://researchr.org/publication/MuKJ09"
  cites: 0
  citedby: 0
  journal: "JFP"
  volume: "19"
  number: "5"
  pages: "545-579"
  kind: "article"
  key: "MuKJ09"