Well-Foundedness and Reductivity
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.
Program Derivation
AoPA — Algebra of Programming in Agda
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.
Constructing List Homomorphism from Left and Right Folds
Back in 2003, my colleagues there were discussing about the third homomorphism theorem — if a function
Deriving a Virtual Machine
Given an interpreter of a small language, derive a virtual machine and a corresponding compiler
Maximum segment sum is back: deriving algorithms for two segment problems with bounded lengths
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]
Maximum Segment Sum, Agda Approved
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…
The Pruning Theorem: Thinning Based on a Loose Notion of Monotonicity
Any preorder
Proving the Thinning Theorem by Fold Fusion
Prove the thinning theorem by fold fusion. Horrifyingly, I could not do it anymore! Have my skills become rusty due to lack of practice in the past few years?
Zipping Half of a List with Its Reversal
Given a list, zip its first half with the reverse of its second half, in only “one and a half” traversals of the list.
Maximum Segment Sum and Density with Bounded Lengths
It may be surprising that variations of the maximum segment sum (MSS) problem, a textbook example for the squiggolists, are still active topics for algorithm designers. These literate Haskell scripts presents a program solving two recently studied variations: computing the maximum sum of segments not longer than an upper-bound, and the maximum density (average) of segments not shorter than a lower-bound. 2007/06/26 Update: fixed binary search.
2007/11/04 Update: linear time algorithm for MSDL.