Page 91 - profile2014.indd

副研究員
穆信成 Shin-Cheng Mu

Associate Research Fellow
D.Phil, Computing Laboratory, University of Oxford
Tel: +886-2-2788-3799 ext. 1730 Fax: +886-2-2782-4814
Email: scm@iis.sinica.edu.tw
http://www.iis.sinica.edu.tw/~scm

Research Description ● 2006 - 2012: assistant research
fellow. IIS, Academia Sinica.
My research interests are mainly focused on formal approaches to program construction. ● 2012 - present: associate research
I have been working on functional and relational approaches to program calculation. The fellow.

general aim of the eld is to stepwise construct, in an algebraic manner, from a problem ● Member of the IFIP Work-

speci cation to an algorithm that solves the problem, and to develop concise notations that ing Group 2.1 on Algorithmic
aid such a development. Languages and Calculi (January
2010 --).
While the relational approach to optimization problems, developed in the late 90’s, was a
major achievement in the eld of program calculation, its natural next step, approxima- ● Steering Committee Member of

tion algorithms, was curiously ignored. We extended the theories of program calculation the Workshop on Generic Pro-
to handle Fully Polynomial-Time Approximation Schemes (FPTAS), a class of approximation gramming (2011 -- 2014).
algorithms with good properties. ● 2003 - 2006: postdoc researcher,
University of Tokyo.
We have found a general theory showing that the traditional “thinning” algorithms can be
seamlessly extended to construct FPTAS. ● 2003: D.Phil, University of Oxford.
● 1996: Bachelor’s degree, National
It is known that once two functions are inferred to form a “Galois connection”, a ubiquitous Chiao-Tung University.
mathematical structure, many useful properties follow.

As an on-going project, we have developed theories that allow us to construct programs

speci ed as the lower adjoint of a Galois connection, and are currently extending the theory to deal with other optimization problems.
While most of the calculations above are traditionally carried out by hand, I have recently shifted my focus to theory and tools of depend-
ently-typed programming and theorem proving. We developed a library, “Algebra of Programming in Agda”, that allows us to encode
algebraic, relational proofs into Agda, a dependently typed programming language, such that proofs can be read by people and also
checked by machine. In another on-going project, we are trying to provide a fully machine-checked proof of an algorithm solving the
“maximally dense segment” problem. While the algorithm appears relatively simple, the proof turns out to be extremely hard.

Publications

1. Shin-Cheng Mu and José Nuno Oliveira, “Programming from 6. Kazutaka Matsuda, Shin-Cheng Mu, Zhenjiang Hu, and Ma-
Galois connections,” Journal of Logic and Algebraic Pro- sato Takeichi, “A grammar-based approach to invertible pro-
gramming 81:680-704., Number 6, 2012. Elsevier. grams,” 19 European Symposium on Programming (ESOP
th
2010), Lecture Notes in Computer Science, 6012, pages 448-
2. Yun-Yan Chi and Shin-Cheng Mu, “Constructing list homo- 467, March 2010.
morphisms from proofs,” The 9 Asian Symposium on Pro-
th
gramming Languages and Systems (APLAS 2011), December 7. S-C. Mu, H-S. Ko, and P. Jansson, “Algebra of programming
2011. in Agda: dependent types for relational program derivation,”
Journal of Functional Programming, volume 19, number 5,
3. Shin-Cheng Mu and Akimasa Morihata, “Generalising and
pages 545-579, September 2009.
Dualising the Third List-Homomorphism Theorem,” Interna-
tional Conference on Functional Programming, pages 385-- 8. Z. Hu, S-C. Mu and M. Takeichi, “A programmable editor
391, September 2011. for developing structured documents based on bidirectional
transformations,” Higher-Order and Symbolic Computation,
4. Shin-Cheng Mu and Jose Nuno Oliveira, “Programming from volume 21, number 1-2, pages 89-118, May 2008.
Galois Connections,” 12 International Conference on Rela-
th
tional and Algebraic Methods in Computer Science (RAMiCS 9. S-C. Mu, H-S. Ko, and P. Jansson, “Algebra of programming
12), Lecture Notes in Computer Science, May 2011. using dependent types,” Mathematics of Program Construc-
tion 2008, Lecture Notes in Computer Science, 5133, pages
5. Shin-Cheng Mu, Yu-Han Lyu, and Akimasa Morihata, “Con- 268-283, July 2008.
structing datatype-generic fully polynomial-time approxi-
th
mation schemes using generalised thinning,” The 6 ACM 10. S-C. Mu, “Maximum segment sum is back: deriving algo-
SIGPLAN workshop on Generic programming (WGP 2010), rithms for two segment problems with bounded lengths,”
Bruno C.d.S. Oliveira and Marcin Zalewski, editor, ACM, Partial Evaluation and Program Manipulation (PEPM ‘08),
pages 97-108, September 2010. pages 31-39, January 2008.

91