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
Termination
Thinning Theorem
Types
XML Streaming
Blog
A Simple Exercise using the Modular Law
May 27, 2008
Prove the following property in point-free style:
S ⊆ C . S ⇐ R ⊆ C . R ∧ S ⊆ R
... [no comments...].
Well-Foundedness and Reductivity
April 25, 2008
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.
... [no comments...].
Well-Founded Recursion and Accessibility
April 20, 2008
Given a relation < that has been shown to be well-founded, we know that a recursively defined function is terminating if its arguments becomes “smaller” with respect to < at each recursive call. We can encode such well-founded recursion in Agda’s style of structural recusion.
... [no comments...].
Terminating Unfolds (2)
April 13, 2008
After seeing our code, Nils Anders Danielsson suggested two improvements. Firstly, to wrap the bound in the seed. Secondly, to define unfoldT↓ using well-founded recursion.
... [no comments...].
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...].
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
- Organising Committee and Lecturer: 2008 Formosan Summer School on Logic, Language, and Computation (2008 「邏輯、語言與計算」暑期研習營暨碩士學分班, FLOLAC '08)
- 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)
- Organising 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!).