Page 166 - My FlipBook
P. 166
研
人 Assistant Research Fellow
員 柯向上 Hsiang-Shang 'Josh' Ko
Faculty DPhil, Computer Science, University of Oxford, United Kingdom
T +886-2-2788-3799 ext. 1719 E joshko@iis.sinica.edu.tw
F +886-2-2782-4814 W www.iis.sinica.edu.tw/pages/joshko
・ Assistant Research Fellow, Institute of Information Science, Academia Sinica, Taiwan
(2019-present)
・ Assistant Professor by Special Appointment, National Institute of Informatics, Japan
(2017-2019)
・ Researcher by Special Appointment, National Institute of Informatics, Japan (2014-2017)
Research Description
I am interested in the discovery of mathematical and logical structures of computation so that they can be manifested in programming
languages and effectively guide the programmer. I approach problems mainly from the perspective of intuitionistic type theory, which
substantially overlaps with functional programming. For theoretical modelling, my weapon of choice is the dependently typed language
Agda; for practical programming, I use the functional language Haskell.
I have been exploring the potential of dependently typed programming, where sophisticated correctness properties and proofs can be
integrated into types and programs, and mechanically verified by type-checking. More interestingly, with an interactive development
environment (like the Emacs mode o ered by Agda) that provides semantic hints in the form of type information, the programmer can gain
better "situation awareness" regarding the meaning of the program being constructed. This is made possible primarily because of inductive
families, and my DPhil thesis developed datatype-generic techniques for improving usability and reusability of inductive families. I also
studied the Algebra of Programming (also known as Bird-Meertens formalism or program calculation) and contributed to its dependently
typed formalisation.
I have also worked on bidirectional transformations for solving consistency maintenance (synchronisation) problems. More speci cally, my
focus was on bidirectional programming, which is largely synonymous with the construction of lenses (introduced by Foster et al at POPL
2005). My main results in this area were built around a small "putback-based" bidirectional programming language BiGUL (Bidirectional
Generic Update Language), about which there were an Agda formalisation, a Haskell port, and an axiomatic semantics that helps to explain
how to think about bidirectional programs unidirectionally. I was also involved in some joint work on the applications of bidirectional
programming, notably the uni cation of parsing and "retentive/re ective" printing with certain guarantees of "well-behavedness".
Publications
1. Zirun Zhu, Hsiang-Shang Ko, Yongzhe Zhang, Pedro Martins, Computer Science, pages 301-320. Springer, 2017. https://doi.
João Saraiva, and Zhenjiang Hu. Unifying parsing and reflective org/10.1007/978-3-319-71237-6_15
printing for fully disambiguated grammars. To appear in New
Generation Computing . https://doi.org/10.1007/s00354-019- 6. Hsiang-Shang Ko and Jeremy Gibbons. Programming with
00082-y ornaments. Journal of Functional Programming, 27:e2, 2017.
https://doi.org/10.1017/S0956796816000307
2. Anthony Anjorin, Thomas Buchmann, Bernhard Westfechtel,
Zinovy Diskin, Hsiang-Shang Ko, Romina Eramo, Georg Hinkel, 7. Hsiang-Shang Ko, Tao Zan, and Zhenjiang Hu. BiGUL: A
Leila Samimi-Dehkordi, and Albert Zündorf. Benchmarking formally verified core language for putback-based bidirectional
bidirectional transformations: Theory, implementation, programming. In Workshop on Partial Evaluation and Program
application, and assessment. Software and Systems Modeling, Manipulation (PEPM), pages 61-72. ACM, 2016. https://doi.
2020. https://doi.org/10.1007/s10270-019-00752-x org/10.1145/2847538.2847544
3. Zhenjiang Hu and Hsiang-Shang Ko. Principles and practice of 8. H s i a n g - S h a n g K o a n d J e r e m y G i b b o n s . R e l a t i o n a l
bidirectional programming in BiGUL. In International Summer algebraic ornaments. In Workshop on Dependently Typed
School on Bidirectional Transformations (Oxford, UK, 25- Programming (DTP), pages 37-48. ACM, 2013. https://doi.
29 July 2016), volume 9715 of Lecture Notes in Computer org/10.1145/2502409.2502413
Science, chapter 4, pages 100-150. Springer, 2018. https://doi.
org/10.1007/978-3-319-79108-1_4 9. Hsiang-Shang Ko and Jeremy Gibbons. Modularising inductive
families. Progress in Informatics, 10:65-88, 2013. https://doi.
4. Hsiang-Shang Ko and Zhenjiang Hu. An axiomatic basis org/10.2201/NiiPi.2013.10.5
for bidirectional programming. Proceedings of the ACM on
Programming Languages, 2(POPL):41, 2018. https://doi. 10. Shin-Cheng Mu, Hsiang-Shang Ko, and Patrik Jansson. Algebra
org/10.1145/3158129 of Programming in Agda: Dependent types for relational program
derivation. Journal of Functional Programming, 19(5):545-579,
5. Yongzhe Zhang, Hsiang-Shang Ko, and Zhenjiang Hu. Palgol: A 2009. https://doi.org/10.1017/S0956796809007345
high-level DSL for vertex-centric graph processing with remote
data access. In Asian Symposium on Programming Languages
and Systems (APLAS), volume 10695 of Lecture Notes in
164
人 Assistant Research Fellow
員 柯向上 Hsiang-Shang 'Josh' Ko
Faculty DPhil, Computer Science, University of Oxford, United Kingdom
T +886-2-2788-3799 ext. 1719 E joshko@iis.sinica.edu.tw
F +886-2-2782-4814 W www.iis.sinica.edu.tw/pages/joshko
・ Assistant Research Fellow, Institute of Information Science, Academia Sinica, Taiwan
(2019-present)
・ Assistant Professor by Special Appointment, National Institute of Informatics, Japan
(2017-2019)
・ Researcher by Special Appointment, National Institute of Informatics, Japan (2014-2017)
Research Description
I am interested in the discovery of mathematical and logical structures of computation so that they can be manifested in programming
languages and effectively guide the programmer. I approach problems mainly from the perspective of intuitionistic type theory, which
substantially overlaps with functional programming. For theoretical modelling, my weapon of choice is the dependently typed language
Agda; for practical programming, I use the functional language Haskell.
I have been exploring the potential of dependently typed programming, where sophisticated correctness properties and proofs can be
integrated into types and programs, and mechanically verified by type-checking. More interestingly, with an interactive development
environment (like the Emacs mode o ered by Agda) that provides semantic hints in the form of type information, the programmer can gain
better "situation awareness" regarding the meaning of the program being constructed. This is made possible primarily because of inductive
families, and my DPhil thesis developed datatype-generic techniques for improving usability and reusability of inductive families. I also
studied the Algebra of Programming (also known as Bird-Meertens formalism or program calculation) and contributed to its dependently
typed formalisation.
I have also worked on bidirectional transformations for solving consistency maintenance (synchronisation) problems. More speci cally, my
focus was on bidirectional programming, which is largely synonymous with the construction of lenses (introduced by Foster et al at POPL
2005). My main results in this area were built around a small "putback-based" bidirectional programming language BiGUL (Bidirectional
Generic Update Language), about which there were an Agda formalisation, a Haskell port, and an axiomatic semantics that helps to explain
how to think about bidirectional programs unidirectionally. I was also involved in some joint work on the applications of bidirectional
programming, notably the uni cation of parsing and "retentive/re ective" printing with certain guarantees of "well-behavedness".
Publications
1. Zirun Zhu, Hsiang-Shang Ko, Yongzhe Zhang, Pedro Martins, Computer Science, pages 301-320. Springer, 2017. https://doi.
João Saraiva, and Zhenjiang Hu. Unifying parsing and reflective org/10.1007/978-3-319-71237-6_15
printing for fully disambiguated grammars. To appear in New
Generation Computing . https://doi.org/10.1007/s00354-019- 6. Hsiang-Shang Ko and Jeremy Gibbons. Programming with
00082-y ornaments. Journal of Functional Programming, 27:e2, 2017.
https://doi.org/10.1017/S0956796816000307
2. Anthony Anjorin, Thomas Buchmann, Bernhard Westfechtel,
Zinovy Diskin, Hsiang-Shang Ko, Romina Eramo, Georg Hinkel, 7. Hsiang-Shang Ko, Tao Zan, and Zhenjiang Hu. BiGUL: A
Leila Samimi-Dehkordi, and Albert Zündorf. Benchmarking formally verified core language for putback-based bidirectional
bidirectional transformations: Theory, implementation, programming. In Workshop on Partial Evaluation and Program
application, and assessment. Software and Systems Modeling, Manipulation (PEPM), pages 61-72. ACM, 2016. https://doi.
2020. https://doi.org/10.1007/s10270-019-00752-x org/10.1145/2847538.2847544
3. Zhenjiang Hu and Hsiang-Shang Ko. Principles and practice of 8. H s i a n g - S h a n g K o a n d J e r e m y G i b b o n s . R e l a t i o n a l
bidirectional programming in BiGUL. In International Summer algebraic ornaments. In Workshop on Dependently Typed
School on Bidirectional Transformations (Oxford, UK, 25- Programming (DTP), pages 37-48. ACM, 2013. https://doi.
29 July 2016), volume 9715 of Lecture Notes in Computer org/10.1145/2502409.2502413
Science, chapter 4, pages 100-150. Springer, 2018. https://doi.
org/10.1007/978-3-319-79108-1_4 9. Hsiang-Shang Ko and Jeremy Gibbons. Modularising inductive
families. Progress in Informatics, 10:65-88, 2013. https://doi.
4. Hsiang-Shang Ko and Zhenjiang Hu. An axiomatic basis org/10.2201/NiiPi.2013.10.5
for bidirectional programming. Proceedings of the ACM on
Programming Languages, 2(POPL):41, 2018. https://doi. 10. Shin-Cheng Mu, Hsiang-Shang Ko, and Patrik Jansson. Algebra
org/10.1145/3158129 of Programming in Agda: Dependent types for relational program
derivation. Journal of Functional Programming, 19(5):545-579,
5. Yongzhe Zhang, Hsiang-Shang Ko, and Zhenjiang Hu. Palgol: A 2009. https://doi.org/10.1017/S0956796809007345
high-level DSL for vertex-centric graph processing with remote
data access. In Asian Symposium on Programming Languages
and Systems (APLAS), volume 10695 of Lecture Notes in
164
