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]
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]
Proving the Church-Rosser Theorem Using a Locally Nameless Representation
Around 2 years ago, for an earlier project of mine (which has not seen its light yet!) in which I had to build a language with variables and prove its properties, I surveyed a number of ways to handle binders. For some background, people have noticed that, when proving properties about a language with bound …
Proving the Church-Rosser Theorem Using a Locally Nameless Representation Read More »
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]