## Fully Polynomial-Time Approximation by Thinning

Code accompanying a forthcoming paper of Yu-Han Lyu, Akimasa Morihata, and me: Constructing Datatype-Generic Fully Polynomial-Time Approximation Schemes Using Generalised Thinning.

Skip to content
# Software

## Fully Polynomial-Time Approximation by Thinning

## Maximally Dense Segments — Code and Proof

## AoPA — Algebra of Programming in Agda

## Push: Improving Heap Residency for Lazy Stream Processing by Concurrency

## Maximum Segment Sum and Density with Bounded Lengths

## Countdown

## Inv

Code accompanying a forthcoming paper of Yu-Han Lyu, Akimasa Morihata, and me: Constructing Datatype-Generic Fully Polynomial-Time Approximation Schemes Using Generalised Thinning.

Code and proof accompanying our forthcoming paper Functional Pearl: Maximally Dense Segments.

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.

Prototype implementation of a language Push, accompanying our recently submitted paper. The prototype is implemented and prepared by Ta-Chung Tsai.

While studying XML stream processing, we noticed that programmers need concurrency to save space, especially in a lazy language. We propose the idea of pushing datatypes — when a pushing closure is demanded, all expressions referring to it are evaluated concurrently to weak head normal forms. The closure is no more alive and may thus be garbage collected.

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.**

Programs and profiling results accompanying the paper Countdown: a case study in origami programming. [GZipped Tarball]

The injective language Inv, together with the language X, the XEditor, and the HaXml embedding. [GZipped Tarball]