Blog

A Survey of Binary Search

February 27, 2010
If you think you know everything you need to know about binary search, but have not read Netty van Gasteren and Wim Feijen’s note The Binary Search Revisited, you should. ... [4 comments...].

A “Side-Swapping” Lemma Regarding Minimum, Using Enriched Indirect Equality

February 13, 2010
If every solution returned by D is no better than some solution returned by X, any optimal solution by X must be no worse than some optimal solution by D “What? How could this be true?” It turned out that the reasoning can be correct, and the proof uses indirect equality in an unusual way. ... [no comments...].

Determining List Steepness in a Homomorphism

July 10, 2009
A list of numbers is called steep if each element is larger than the sum of elements to its right. It is an example we often use when we talk about tupling. Can we determine the steepness of a list by a list homomorphism? ... [8 comments...].

The Windowing Technique for Longest Segment Problems

June 20, 2009
Reviewing Zantema’s “windowing” technique for computing the longest segment of the input that satisfies a suffix-closed predicate. ... [no comments...].

Longest Segment Satisfying Suffix and Overlap-Closed Predicates

June 7, 2009
Translating Zantema’s work to Bird-Meertens style, to compute the longest consecutive segment of the input that satisfies a predicate that is suffix and overlap-closed. ... [no comments...].

[All blog posts...]

Software

  • 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.
  • Push: Improving Heap Residency for Lazy Stream Processing by Concurrency: 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
  • 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
  • Countdown: Programs and profiling results accompanying the paper Countdown: a case study in origami programming. [GZipped Tarball]
  • Inv: The injective language Inv, together with the language X, the XEditor, and the HaXml embedding. [GZipped Tarball]

Academic Activities

Programme Committee member: Summerschool organisation:
Teaching:

Colleagues

Research assistants:
  • Yun-Yan Chi (jaiyalas) 郗昀彥,
  • Jian-Xin Lin (godfat) 林建欣,
  • Yu-Han Lyu 呂昱翰,
  • Ta-Chung Tsai 蔡大中.
Previous research assistants: