Page 89 - 2017 Brochure
P. 89
研究員
穆信成 Shin-Cheng Mu
Associate Research Fellow
DPhil (Ph.D.), 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/pages/scm
• Member, IFIP Working Group 2.1 on Algorithmic Languages and Calculi (2010-present)
• Organizer, Lecturer, Formosan Summer School on Logic, Language, and Computation, Taipei, Taiwan (2007-present)
• Guest Editor, Science of Computer Programming. Special Issue for PEPM 2013 (2013-2014)
• Steering Committee Chair, Workshop of Generic Programming Steering Committee (2013-2014)
• Steering Committee Member, Workshop on Generic Programming (2011-2013)
• Co-Chair, ACM SIGPLAN 2013 Workshop on Partial Evaluation and Program Manipulation (PEPM '13), (2013)
• PC Co-Chair, Seventh Workshop on Generic Programming (WGP '11), (2011)
• Postdoctoral Researcher, University of Tokyo, Information Processing Lab, Japan (2003-2006)
Research Description algebraic proofs that can be read by people may also be checked
by machine. We expect that this helps to improve correctness of
The main theme of my research is taking formal approaches to program derivation and allows derivation to scale up to much larger
program construction. In particular, I am interested in functional programs.
and relational approaches to program calculation. The general
approach is to begin with a problem specification and stepwise On a more theoretical note, we have developed theories that allow
construct, in an algebraic manner, an algorithm that solves the us to use Galois connection (GC) as a specification, from which we
problem. Our most recent project involves an elegant algorithm may calculate an implementation of the function. The technique is
pattern which we nickname the “queueing and glueing” algorithm. applied to optimization problems, many of which can be specified
Additional works on program calculation include the maximally as a GC. By doing so, we considerably simplify previous theories
dense segment problem, list homomorphism, and applying on calculation of optimization problems. On the practical side, we
the “thinning” approach in relational program calculation to developed the “modular reifiable matching” technique which is
approximation algorithms, among others. similar to Datatypes à la Carte, but has advantages that can help
with extensibility, modularity and reuse.
In recent years I have also been studying dependently typed
programming and theorem proving. While program calculation
is traditionally carried out by hand, we developed a library AoPA
(Algebra of Programming in Agda) that allows one to encode
algebraic, relational proofs into Agda, a dependently typed
programming language. We thus gain the best of both worlds: clear
Publications 7. S-C Mu and J. N. Oliveira, “Programming from Galois connections,”
Journal of Logic and Algebraic Programming, volume 81, number 6,
1. S-C. Mu, Y-H. Chiang, and Y-H. Lyu, “Queueing and glueing pages 680–704, August 2012.
for optimal partitioning,” International Conference on Functional
Programming (ICFP 2016), Eijiro Sumii, editor, ACM Press, pages 8. Y-Y. Chi and S-C. Mu, “Constructing list homomorphisms from
158-167, September 2016. proofs,” The 9th Asian Symposium on Programming Languages and
Systems (APLAS 2011), December 2011.
2. Y-H. Chiang, S-C. Mu, “Formal derivation of greedy algorithms from
relational specifications: a tutorial,” Journal of Logic and Algebraic 9. S-C. Mu and A. Morihata, “Generalising and dualising the third list-
Programming, volume 85, number 5, Part 2, pages 879–905, August homomorphism theorem,” International Conference on Functional
2016. Programming, pages 385--391, September 2011.
3. S. Curtis, S-C. Mu, “Calculating a linear-time solution to the densest- 10. S-C. Mu, H-S. Ko, and P. Jansson, “Algebra of programming in
segment problem,” Journal of Functional Programming, volume 25, Agda: dependent types for relational program derivation,” Journal
number 0, pages e22 (32 pages), December 2015. of Functional Programming, volume 19, number 5, pages 545-579,
September 2009.
4. B. C. d. S. Oliveira, S-C. Mu, S-H. You, “Modular reifiable matching:
a list-of-functors approach to two-level types,” Haskell Symposium
2015, B. Lippmeier, editor, pages 82-93, September 2015.
5. S-C. Mu, Y-H. Lyu, and A. Morihata, “Approximate by thinning:
deriving fully polynomial-time approximation schemes,” Science
of Computer Programming, volume 98, number 4, pages 484–515,
February 2015.
6. S-C. Mu, T-W. Chen, “Functional pearl: Nearest shelters in
Manhattan,” Programming Languages and Systems, Lecture Notes in
Computer Science, 8858, pages 159-175, November 2014.
87
穆信成 Shin-Cheng Mu
Associate Research Fellow
DPhil (Ph.D.), 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/pages/scm
• Member, IFIP Working Group 2.1 on Algorithmic Languages and Calculi (2010-present)
• Organizer, Lecturer, Formosan Summer School on Logic, Language, and Computation, Taipei, Taiwan (2007-present)
• Guest Editor, Science of Computer Programming. Special Issue for PEPM 2013 (2013-2014)
• Steering Committee Chair, Workshop of Generic Programming Steering Committee (2013-2014)
• Steering Committee Member, Workshop on Generic Programming (2011-2013)
• Co-Chair, ACM SIGPLAN 2013 Workshop on Partial Evaluation and Program Manipulation (PEPM '13), (2013)
• PC Co-Chair, Seventh Workshop on Generic Programming (WGP '11), (2011)
• Postdoctoral Researcher, University of Tokyo, Information Processing Lab, Japan (2003-2006)
Research Description algebraic proofs that can be read by people may also be checked
by machine. We expect that this helps to improve correctness of
The main theme of my research is taking formal approaches to program derivation and allows derivation to scale up to much larger
program construction. In particular, I am interested in functional programs.
and relational approaches to program calculation. The general
approach is to begin with a problem specification and stepwise On a more theoretical note, we have developed theories that allow
construct, in an algebraic manner, an algorithm that solves the us to use Galois connection (GC) as a specification, from which we
problem. Our most recent project involves an elegant algorithm may calculate an implementation of the function. The technique is
pattern which we nickname the “queueing and glueing” algorithm. applied to optimization problems, many of which can be specified
Additional works on program calculation include the maximally as a GC. By doing so, we considerably simplify previous theories
dense segment problem, list homomorphism, and applying on calculation of optimization problems. On the practical side, we
the “thinning” approach in relational program calculation to developed the “modular reifiable matching” technique which is
approximation algorithms, among others. similar to Datatypes à la Carte, but has advantages that can help
with extensibility, modularity and reuse.
In recent years I have also been studying dependently typed
programming and theorem proving. While program calculation
is traditionally carried out by hand, we developed a library AoPA
(Algebra of Programming in Agda) that allows one to encode
algebraic, relational proofs into Agda, a dependently typed
programming language. We thus gain the best of both worlds: clear
Publications 7. S-C Mu and J. N. Oliveira, “Programming from Galois connections,”
Journal of Logic and Algebraic Programming, volume 81, number 6,
1. S-C. Mu, Y-H. Chiang, and Y-H. Lyu, “Queueing and glueing pages 680–704, August 2012.
for optimal partitioning,” International Conference on Functional
Programming (ICFP 2016), Eijiro Sumii, editor, ACM Press, pages 8. Y-Y. Chi and S-C. Mu, “Constructing list homomorphisms from
158-167, September 2016. proofs,” The 9th Asian Symposium on Programming Languages and
Systems (APLAS 2011), December 2011.
2. Y-H. Chiang, S-C. Mu, “Formal derivation of greedy algorithms from
relational specifications: a tutorial,” Journal of Logic and Algebraic 9. S-C. Mu and A. Morihata, “Generalising and dualising the third list-
Programming, volume 85, number 5, Part 2, pages 879–905, August homomorphism theorem,” International Conference on Functional
2016. Programming, pages 385--391, September 2011.
3. S. Curtis, S-C. Mu, “Calculating a linear-time solution to the densest- 10. S-C. Mu, H-S. Ko, and P. Jansson, “Algebra of programming in
segment problem,” Journal of Functional Programming, volume 25, Agda: dependent types for relational program derivation,” Journal
number 0, pages e22 (32 pages), December 2015. of Functional Programming, volume 19, number 5, pages 545-579,
September 2009.
4. B. C. d. S. Oliveira, S-C. Mu, S-H. You, “Modular reifiable matching:
a list-of-functors approach to two-level types,” Haskell Symposium
2015, B. Lippmeier, editor, pages 82-93, September 2015.
5. S-C. Mu, Y-H. Lyu, and A. Morihata, “Approximate by thinning:
deriving fully polynomial-time approximation schemes,” Science
of Computer Programming, volume 98, number 4, pages 484–515,
February 2015.
6. S-C. Mu, T-W. Chen, “Functional pearl: Nearest shelters in
Manhattan,” Programming Languages and Systems, Lecture Notes in
Computer Science, 8858, pages 159-175, November 2014.
87
