Research
-
λ calculus
Agda
Bidirectional Updating
Burrows-Wheeler Transform
Concurrency
Converse-of-a-Function Theorem
Curry-Howard
Data Structure
Dependent Type
GADT
Greedy Theorem
Haskell
HaXML
List Homomorphism
Logic
Logic Programming
Program Derivation
Program Inversion
Quantum Programming
Quine
Regular Expression
Segment Problems
Thinning Theorem
Types
XML Streaming
Blog
Terminating Unfolds (1)
April 8, 2008
I hope to come up with a variation of unfoldr which, given a proof of well-foundedness, somehow passes the termination check.
... [no comments...].
Constructing List Homomorphism from Left and Right Folds
February 10, 2008
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 ⊚.
... [1 comment...].
S Combinator is Injective, with Proofs
December 5, 2007
By chance, I came upon a blog entry by Masahiro Sakai (酒井政裕) in which he, after reading my short comment “Do you know that the S combinator is injective?”, tried to construct the inverse of S and showed that S⁻¹ ○ S = id in, guess what, Agda!
... [5 comments...].
Deriving a Virtual Machine
November 26, 2007
Given an interpreter of a small language, derive a virtual machine and a corresponding compiler
... [5 comments...].
Maximum Segment Sum, Agda Approved
November 11, 2007
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…
... [2 comments...].
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 in Agda: a Case Study” (MPC 2008, to appear soon) 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: Ninth International Conference on Mathematics of Program Construction (MPC '08)
- Programme Committee: ACM SIGPLAN 2008 Workshop on Partial Evaluation and Program Manipulation (PEPM '08)
- Program Committee and Lecturer: 2007 Formosan Summer School on Logic, Language, and Computation (2007 「邏輯、語言與計算」暑期研習營暨碩士學分班, FLOLAC '07)
- Programme Committee: The Fifth ASIAN Symposium on Programming Language and Systems (APLAS 2007)
- Programme Committee: 2006 Haskell Workshop
- Programme Committee: 8th International Conference on Mathematics of Program Construction (MPC '06)
Colleagues
Research assistants:- Yun-Yan Chi (jaiyalas) 郗昀彥
- Luke Hsueh 薛共和
- Yao-Xian Huang (ephesians) 黃耀賢
- Josh Ko 柯向上
- Jian-Xin Lin (godfat) 林建欣
- Gou-Zhan Huang 黃國展 (Aug. 2006 - Apr. 2007). Prime View International 元太科技.
- Ta-Chung Tsai 蔡大中 (Jul. 2007 - Nov. 2007). Military Service (fingers crossed!).