Publications

Declarative pearl: deriving monadic quicksort

Shin-Cheng Mu and Tsung-Ju Chiang. In Functional and Logic Programming (FLOPS), Keisuke Nakano and Konstantinos Sagonas, editors. April 2020.
[PDF |Agda Proofs]

Handling local state with global state

Koen Pauwels, Tom Schrijvers and Shin-Cheng Mu. In Mathematics of Program Construction (MPC), Graham Hutton, editor, pp. 18-44. Springer, October 2019.
[PDF]

Calculating a backtracking algorithm: an exercise in monadic program derivation

Shin-Cheng Mu. Tech. Report TR-IIS-19-003, Institute of Information Science, Academia Sinica, June 2019.
[PDF]

Equational reasoning for non-determinism monad: the case of Spark aggregation

Shin-Cheng Mu. Tech. Report TR-IIS-19-002, Institute of Information Science, Academia Sinica, June 2019.
[PDF]

Functional pearl: folding polynomials of polynomials

Chen-Mou Cheng, Ruey-Lin Hsu and Shin-Cheng Mu. In Functional and Logic Programming (FLOPS), John Gallagher and Martin Sulzmann, editors, pp 68-83, 2018.

Type safe Redis queries — a case study of type-level programming in Haskell

Ting-Yan Lai, Tyng-Ruey Chuang, and Shin-Cheng Mu. In 2nd Workshop on Type-Driven Development (TyDe), 2017.
[PDF]

An executable sequential specification for Spark aggregation

Yu-Fang Chen, Chih-Duo Hong, Ondřej Lengál, Shin-Cheng Mu, Nishant Sinha, and Bow-Yaw Wang. Networked Systems (NETYS), pp. 421-438. 2017.
[PDF|Code|Supplementary Proofs]

Queueing and glueing for optimal partitioning

Shin-Cheng Mu, Yu-Hsi Chiang, and Yu-Han Lyu. In the 21st ACM SIGPLAN International Conference on Functional Programming (ICFP 2016), Eijiro Sumii, editor, pages 158-167. ACM Press, Sep. 2016.
[Paper | Code]

Formal derivation of greedy algorithms from relational specifications: a tutorial

Yu-Hsi Chiang, Shin-Cheng Mu. Journal of Logical and Algebraic Methods in Programming, 85(5), Part 2, pp 879-905, August 2016.
[Paper(doi:10.1016/j.jlamp.2015.12.003) | Code]

Modular reifiable matching: a list-of-functors approach to two-level types

Bruno C. d. S. Oliveira, Shin-Cheng Mu, and Shu-Hung You. In the 8th ACM SIGPLAN Symposium on Haskell (Haskell 2015), pages 82-93. Sep. 2015.
[Paper (doi: 10.1145/2804302.2804315)| Code]

Calculating a linear-time solution to the densest segment problem

Sharon Curtis and Shin-Cheng Mu. Calculating a linear-time solution to the densest segment problem. Journal of Functional Programming, Vol. 25, 2015.
[Paper (doi: 10.1017/S095679681500026X)| Supplementary Proofs | Code]

The problem of finding a densest segment of a list is similar to the well-known maximum segment sum problem, but its solution is surprisingly challenging. We give a general specification of such problems, and formally develop a linear-time online solution, using a sliding window style algorithm. The development highlights some elegant properties of densities, involving partitions that are decreasing and all right-skew.

Programming from Galois connections

Shin-Cheng Mu and José Nuno Oliveira. Programming from Galois connections. In the Journal of Logic and Algebraic Programming , Vol 81(6), pages 680–704, August 2012.
[PDF]

Constructing list homomorphisms from proofs

Yun-Yan Chi and Shin-Cheng Mu. Constructing list homomorphisms from proofs. In the 9th Asian Symposium on Programming Languages and Systems (APLAS 2011), LNCS 7078, pages 74-88. [PDF]

Generalising and dualising the third list-homomorphism theorem

Shin-Cheng Mu and Akimasa Morihata. Generalising and dualising the third list-homomorphism theorem. In the 16th ACM SIGPLAN International Conference on Functional Programming (ICFP 2011), pages 385-391.
[PDF]

Programming from Galois connections — principles and applications

Shin-Cheng Mu and José Nuno Oliveira. Programming from Galois connections — principles and applications. Technical Report TR-IIS-10-009, Academia Sinica, December 2010.
[PDF]

Programming from Galois connections

Shin-Cheng Mu and José Nuno Oliveira. Programming from Galois connections. In the 12th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS #12), LNCS 6663, pages 294-313. May 30 – June 3, 2011.
[PDF]

Constructing datatype-generic fully polynomial-time approximation schemes using generalised thinning

Shin-Cheng Mu, Yu-Han Lyu, and Akimasa Morihata. Constructing datatype-generic fully polynomial-time approximation schemes using generalised thinning. In the 6th ACM SIGPLAN workshop on Generic programming (WGP 2010), pages 97-108, Sep. 2010. [PDF]

Functional pearl: maximally dense segments

Sharon Curtis and Shin-Cheng Mu. Functional pearl: maximally dense segments. Submitted.
[PDF]

A grammar-based approach to invertible programs

Kazutaka Matsuda, Shin-Cheng Mu, Zhenjiang Hu, and Masato Takeichi. A grammar-based approach to invertible programs. In 19th European Symposium on Programming (ESOP 2010), LNCS 6012, pp 448-467, March 2010.
[PDF]

Algebra of programming in Agda: dependent types for relational program derivation

S-C. Mu, H-S. Ko, and P. Jansson. Algebra of programming in Agda: dependent types for relational program derivation. In Journal of Functional Programming, Vol. 19(5), pp. 545-579. Sep. 2009. [PDF]

Algebra of programming using dependent types

S-C. Mu, H-S. Ko, and P. Jansson. Algebra of programming using dependent types. In Mathematics of Program Construction 2008, LNCS 5133, pp 268-283. July 2008.
Superseded by the extended version for Journal of Functional Programming.
[PDF]

A programmable editor for developing structured documents based on bidirectional transformations

Z. Hu, S-C. Mu and M. Takeichi, A programmable editor for developing structured documents based on bidirectional transformations. Higher-Order and Symbolic Computation, Vol 21(1-2), pp 89-118, May 2008.
[PDF]

XML stream processing using a lazy concurrent language

S-C. Mu, T-C. Tsai, and K. Nakano. XML stream processing using a lazy concurrent language. In Programming Language Techniques for XML (PLAN-X 2008). January 2008.
[PDF]

Maximum segment sum is back: deriving algorithms for two segment problems with bounded lengths

S-C. Mu. Maximum segment sum is back: deriving algorithms for two segment problems with bounded lengths. In Partial Evaluation and Program Manipulation (PEPM ’08), pp 31-39. January 2008.
[PDF] [GZipped Postscript]

A pushdown machine for recursive XML processing

K. Nakano and S-C. Mu. A pushdown machine for recursive XML processing. In The Fourth Asian Symposium on Programming Language and Systems, LNCS 4279, pp. 340-356, November 2006.
[PDF]

Bidirectionalizing tree transformation languages: a case study

S-C. Mu, Z. Hu and M. Takeichi, Bidirectionalizing tree transformation languages: a case study. In JSSST Computer Software (コンピュータソフトウェア) Vol. 23(2), pp. 129-141, 2006.
[PDF]

Countdown: a case study in origami programming

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]

Inverting the Burrows-Wheeler transform

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.
[
PDF][GZipped Postscript]

An algebraic approach to bidirectional updating

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]

A programmable editor for developing structured documents based on bidirectional transformations

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]

An injective language for reversible computation

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]

Theory and applications of inverting functions as folds.

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.
[PDF][GZipped Postscript]

Rebuilding a tree from its traversals: a case study of program inversion

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]

A Calculational Approach to Program Inversion

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

Inverting functions as folds

S-C. Mu and R. S. Bird, Inverting functions as folds. In Sixth International Conference on Mathematics of Program Construction, Dagstuhl, Germany, July 2002
[GZipped Postscript]

Algebraic methods for optimisation problems

R. S. Bird, J. Gibbons and S-C. Mu, Algebraic methods for optimisation problems. In Algebraic and Coalgebraic Methods in the Mathematics of Program Construction, LNCS 2297, pp. 281-307, January 2002.
[PDF]

Quantum functional programming

S-C. Mu and R. S. Bird, Quantum functional programming. In 2nd Asian Workshop on Programming Languages and Systems , KAIST, Dajeaon, Korea, December 17-18, 2001.
[GZipped Postscript]

Inverting the Burrows-Wheeler Transform

R. S. Bird and S-C. Mu, Inverting the Burrows-Wheeler Transform. In ACM SIGPLAN 2001 Haskell Workshop, Firenze, Italy, September 2001.
Superseded by the extended version for Journal of Functional Programming.

On building trees with minimum height, relationally

S-C. Mu and R. S. Bird, On building trees with minimum height, relationally. In First Asian Workshop on Programming Languages and Systems, Singapore, December 2000.
[GZipped Postscript]

Algebraic Methods for Optimisation Problems (Transfering dissertation)

S-C. Mu, Algebraic Methods for Optimisation Problems. Transfering dissertation.

Optimisation problems in logic programming: an algebraic approach

S. Seres and S-C. Mu, Optimisation problems in logic programming: an algebraic approach. In Proceedings of LPSE’00, July 2000.
[GZipped Postscript]

Out-of-core functional programming with type-based primitives

T-R. Chuang and S-C. Mu, Out-of-core functional programming with type-based primitives. In 2nd International Workshop on Practical Aspects of Declarative Languages, January 2000.
[GZipped Postscript]