Page 184 - My FlipBook
P. 184
研
人 Associate Research Fellow
員 穆信成 Shin-Cheng Mu
Faculty DPhil (Ph.D.), Computing Laboratory, University of Oxford, United Kingdom
T +886-2-2788-3799 ext.730 E scm@iis.sinica.edu.tw
F +886-2-2782-4814 W www.iis.sinica.edu.tw/pages/scm
・ Steering Committee Member, International Conference on Functional Programming
(2019/09 - 2023/09)
・ Member, IFIP Working Group 2.1 on Algorithmic Languages and Calculi (2010/01-present)
・ Organizer, Lecturer, Formosan Summer School on Logic, Language, and Computation,
Taipei, Taiwan (2007-present)
・ Guest Editor, Science of Computer Programming. Speicial Issue for PEPM 2013 (2013/01-
2014/06)
・ Steering Committee Chair, Workshop of Generic Programming Steering Committee
(2013/10-2014/10)
・ Co-Chair, ACM SIGPLAN 2013 Workshop on Partial Evaluation and Program Manipulation
(PEPM '13), (2013/01-2013/01)
・ PC Co-Chair, Seventh Workshop on Generic Programming (WGP '11), (2011/09-2011/09)
・ Postdoc, University of Tokyo, Information Processing Lab, Japan (2003/6-2006/1)
Research Description
The main theme of my research is about formal approaches to program construction, in particular, functional and relational approaches to
program calculation. The general aim of the eld is to stepwise construct from a problem speci cation, in an algebraic manner, an algorithm
that solves the problem. One example involves an elegant algorithm pattern which we nickname "queueing and glueing'' algorithm. In
recent years I am also experimenting with derivation of monadic programs. I believe it will be a good alternative to relational program
calculation.
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 algebraic proofs that can be read by
people may also checked by machine. We hope this helps to improve correctness of program derivation and allows derivation to scale up to
much larger programs.
On a more theoretical side, we developed theories that allow us to use Galois connection (GC) as a speci cation, from which we may calculate
an implementation of the function. The technique is applied to optimisation problems, many of which can be speci ed as a GC, and by doing
so we considerably simplified previous theories on calculation of optimisation problems. On the practical side, we developed "modular
rei able matching" Datatypes à la Carte that has advantages that help with extensibility, modularity and reuse.
Publications from relational specifications: a tutorial," Journal of Logic and
Algebraic Programming, volume 85, number 5, Part 2, pages 879-
1. S-C. Mu and T-J. Chiang, "Declarative pearl: deriving monadic 905, August 2016.
quicksort." In Functional and Logic Programming (FLOPS),
Keisuke Nakano and Konstantinos Sagonas, editors. April 2020. 7. S. Curtis, S-C. Mu, "Calculating a linear-time solution to the
densest-segment problem," Journal of Functional Programming,
2. K. Pauwels, T. Schrijvers and S-C. Mu, "Handling local state with volume 25, number 0, pages e22 (32 pages), December 2015.
global state." In Mathematics of Program Construction (MPC),
Graham Hutton, editor, pp. 18-44. Springer, October 2019. 8. B. C. d. S. Oliveira, S-C. Mu, S-H. You, "Modular reifiable
matching: a list-of-functors approach to two-level types," Haskell
3. C-M. Cheng, R-L. Hsu, and S-C. Mu, "Functional pearl: Symposium 2015, B. Lippmeier, editor, pages 82-93, September
folding polynomials of polynomials." In Functional and Logic 2015.
Programming (FLOPS), John Gallagher and Martin Sulzmann,
editors, pp 68-83, 2018. 9. S-C. Mu, Y-H. Lyu, and A. Morihata, "Approximate by thinning:
deriving fully polynomial-time approximation schemes," Science
4. Y-F. Chen, C-D. Hong, O. Lengál, S-C. Mu, N. Sinha, and of Computer Programming, volume 98, number 4, pages 484-
B-Y. Wang, "An executable sequential specification for Spark 515, February 2015.
aggregation". Networked Systems (NETYS), pp. 421-438. 2017.
10. S-C. Mu, T-W. Chen, "Functional pearl: Nearest shelters in
5. S-C. Mu, Y-H. Chiang, and Y-H. Lyu, "Queueing and glueing for Manhattan," Programming Languages and Systems, Lecture
optimal partitioning," International Conference on Functional Notes in Computer Science, 8858, pages 159-175, November
Programming (ICFP 2016), Eijiro Sumii, editor, ACM Press , 2014.
pages 158-167, September 2016.
6. Y-H. Chiang, S-C. Mu, "Formal derivation of greedy algorithms
182
人 Associate Research Fellow
員 穆信成 Shin-Cheng Mu
Faculty DPhil (Ph.D.), Computing Laboratory, University of Oxford, United Kingdom
T +886-2-2788-3799 ext.730 E scm@iis.sinica.edu.tw
F +886-2-2782-4814 W www.iis.sinica.edu.tw/pages/scm
・ Steering Committee Member, International Conference on Functional Programming
(2019/09 - 2023/09)
・ Member, IFIP Working Group 2.1 on Algorithmic Languages and Calculi (2010/01-present)
・ Organizer, Lecturer, Formosan Summer School on Logic, Language, and Computation,
Taipei, Taiwan (2007-present)
・ Guest Editor, Science of Computer Programming. Speicial Issue for PEPM 2013 (2013/01-
2014/06)
・ Steering Committee Chair, Workshop of Generic Programming Steering Committee
(2013/10-2014/10)
・ Co-Chair, ACM SIGPLAN 2013 Workshop on Partial Evaluation and Program Manipulation
(PEPM '13), (2013/01-2013/01)
・ PC Co-Chair, Seventh Workshop on Generic Programming (WGP '11), (2011/09-2011/09)
・ Postdoc, University of Tokyo, Information Processing Lab, Japan (2003/6-2006/1)
Research Description
The main theme of my research is about formal approaches to program construction, in particular, functional and relational approaches to
program calculation. The general aim of the eld is to stepwise construct from a problem speci cation, in an algebraic manner, an algorithm
that solves the problem. One example involves an elegant algorithm pattern which we nickname "queueing and glueing'' algorithm. In
recent years I am also experimenting with derivation of monadic programs. I believe it will be a good alternative to relational program
calculation.
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 algebraic proofs that can be read by
people may also checked by machine. We hope this helps to improve correctness of program derivation and allows derivation to scale up to
much larger programs.
On a more theoretical side, we developed theories that allow us to use Galois connection (GC) as a speci cation, from which we may calculate
an implementation of the function. The technique is applied to optimisation problems, many of which can be speci ed as a GC, and by doing
so we considerably simplified previous theories on calculation of optimisation problems. On the practical side, we developed "modular
rei able matching" Datatypes à la Carte that has advantages that help with extensibility, modularity and reuse.
Publications from relational specifications: a tutorial," Journal of Logic and
Algebraic Programming, volume 85, number 5, Part 2, pages 879-
1. S-C. Mu and T-J. Chiang, "Declarative pearl: deriving monadic 905, August 2016.
quicksort." In Functional and Logic Programming (FLOPS),
Keisuke Nakano and Konstantinos Sagonas, editors. April 2020. 7. S. Curtis, S-C. Mu, "Calculating a linear-time solution to the
densest-segment problem," Journal of Functional Programming,
2. K. Pauwels, T. Schrijvers and S-C. Mu, "Handling local state with volume 25, number 0, pages e22 (32 pages), December 2015.
global state." In Mathematics of Program Construction (MPC),
Graham Hutton, editor, pp. 18-44. Springer, October 2019. 8. B. C. d. S. Oliveira, S-C. Mu, S-H. You, "Modular reifiable
matching: a list-of-functors approach to two-level types," Haskell
3. C-M. Cheng, R-L. Hsu, and S-C. Mu, "Functional pearl: Symposium 2015, B. Lippmeier, editor, pages 82-93, September
folding polynomials of polynomials." In Functional and Logic 2015.
Programming (FLOPS), John Gallagher and Martin Sulzmann,
editors, pp 68-83, 2018. 9. S-C. Mu, Y-H. Lyu, and A. Morihata, "Approximate by thinning:
deriving fully polynomial-time approximation schemes," Science
4. Y-F. Chen, C-D. Hong, O. Lengál, S-C. Mu, N. Sinha, and of Computer Programming, volume 98, number 4, pages 484-
B-Y. Wang, "An executable sequential specification for Spark 515, February 2015.
aggregation". Networked Systems (NETYS), pp. 421-438. 2017.
10. S-C. Mu, T-W. Chen, "Functional pearl: Nearest shelters in
5. S-C. Mu, Y-H. Chiang, and Y-H. Lyu, "Queueing and glueing for Manhattan," Programming Languages and Systems, Lecture
optimal partitioning," International Conference on Functional Notes in Computer Science, 8858, pages 159-175, November
Programming (ICFP 2016), Eijiro Sumii, editor, ACM Press , 2014.
pages 158-167, September 2016.
6. Y-H. Chiang, S-C. Mu, "Formal derivation of greedy algorithms
182
