Niche Computing Science

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!

Z. Hu, S-C. Mu and M. Takeichi, A programmable editor for developing structured documents based on bidirectional transformations. Higher-Order and Symbolic Computation, to appear.
[PDF]

R. S. Bird and S-C. Mu, Countdown: a case study in origami programming. In Journal of Functional Programming Vol. 15(5), pp. 679-702, 2005.
[GZipped Postscript]

R. S. Bird and S-C. Mu, Inverting the Burrows-Wheeler transform. In Journal of Functional Programming Vol. 14(6) Special Issue on Functional Pearls, pp. 603-612, Novermber 2004.
[GZipped Postscript]

S-C. Mu, Z. Hu and M. Takeichi. An algebraic approach to bidirectional updating. In The Second Asian Symposium on Programming Language and Systems, pp. 2-18. November 2004.
[PDF]

Z. Hu, S-C. Mu and M. Takeichi, A programmable editor for developing structured documents based on bidirectional transformations. In Partial Evaluation and Semantics-Based Program Manipulation, pp. 178-189. August 2004.
[PDF]

S-C. Mu, Z. Hu and M. Takeichi, An injective language for reversible computation. In Mathematics of Program Construction 2004, LNCS 3125, pp. 289-313, July 2004.
[PDF]

S-C. Mu and R. S. Bird, Theory and applications of inverting functions as folds. In Science of Computer Programming Vol. 51 Special Issue for Mathematics of Program Construction 2002, pp. 87-116, 2003.
[GZipped Postscript]

S-C. Mu and R. S. Bird, Rebuilding a tree from its traversals: a case study of program inversion. In The First Asian Symposium on Programming Languages and Systems, LNCS 2895, pp. 265-282, Bejing, 2003.
[GZipped Postscript]

S-C. Mu, A Calculational Approach to Program Inversion. D.Phil Thesis. Oxford University Computing Laboratory. March 2003
[GZipped Postscript][PDF]