Shin-Cheng Mu

aopa. Algebra of Programming in Agda: Dependent Types for Relational Program Derivation

foundations-harper. Agda proofs for some of the theorems in Robert Harper's Practical Foundations of Programming Languages.

mrm. Modular Reifiable Matching, A List-of-Functors Approach to Two-Level Types

fpcr. Functional Program Construction and Reasoning

monad-reasoning. TeX

mds. Code and Proofs Related to the Paper "Functional Pearl: Finding a Densest Segment"

guabao-paper. TeX

plfp. CSS

acane. ACANE: Algebraic Calculation and Normalised Equations