for the few of us.

How can I introduce accumulating parameters to derive the linear-time, tail recursive implementation of fib.

S-C. Mu, H-S. Ko, and P. Jansson. Algebra of programming using dependent types. In Mathematics of Program Construction 2008, LNCS 5133, pp 268-283. July 2008.
[PDF]

Prove the following property in point-free style:

$S\; \subseteq \; C\; .\; S\; \; \Leftarrow \; \; R\; \subseteq \; C\; .\; R\; \; \wedge \; \; S\; \subseteq \; R$

It seems that reductivity of Doornbos and Backhouse is in fact accessibility, which is often taken by type theorists to be an alternative definition of well-foundedness.

The AoPA library allows one to encode Algebra of Programming style program derivation, both functional and relational, in Agda, accompanying the paper Algebra of Programming Using Dependent Types (MPC 2008) developed in co-operation with Hsiang-Shang Ko and Patrik Jansson.

Back in 2003, my colleagues there were discussing about the third homomorphism theorem — if a function f can be expressed both as a foldr and a foldl, there exists some associative binary operator ⊚ such that f can be computed from the middle. The aim was to automatically construct ⊚.

Given an interpreter of a small language, derive a virtual machine and a corresponding compiler

S-C. Mu. Maximum segment sum is back: deriving algorithms for two segment problems with bounded lengths. In Partial Evaluation and Program Manipulation (PEPM ‘08), pp 31-39. January 2008.
[PDF] [GZipped Postscript]

To practise using the Logic.ChainReasoning module in Agda, Josh proved the foldr-fusion theorem, and I thought it would be an small exercise over the weekend to start off where he finished…

Any preorder R induces a lax preorder ∋ . R. If a relation S is monotonic on R∘, it is monotonic on lax preorder ∋ . R. Furthermore, prune (∋ . R) = thin R. Therefore, pruning is a generalisation of thinning. We need the notion of lax preorders because, for some problems, the generating relation S is monotonic on a lax preorder, but not a preorder.