Page 136 - My FlipBook
P. 136
大
實室 Programming Languages and Formal
驗
Research Laboratories Methods Laboratory
Research Faculty
Yu-Fang Chen / Chair The Programming Languages and Formal Methods research group develops techniques to
ensure program correctness. Our research into programming languages focuses on syntactic,
Research Fellow semantic, and pragmatic issues in the development of correct programs. Our work on formal
methods emphasizes the algorithmic, computational, and practical aspects of realistic program
Bow-Yaw Wang analyses. We apply mathematical and formal techniques to our investigations of research
problems. We also aim to develop tools and methodologies that can help developers write
Research Fellow code correctly.
Hsiang-Shang Ko I. Reasoning and Derivation of Functional and Monadic Programs
Assistant Research Purely functional languages, in which functions are true mathematical functions, offer
Fellow a simple model of computation in which programs can be understood as mathematical
equations whose properties can be proved using mathematical tools including induction.
Tyng-Ruey Chuang An e cient program can be derived from a program speci cation by stepwise equational
reasoning, whereby every step is justified by a theorem. This technique, called "program
Associate Research derivation", aims to provide formalization and patterns that help programmers to develop
Fellow programs and their correctness proofs at the same time. We have published some
interesting case studies of derivation, including approximation algorithms and algorithms
Shin-Cheng Mu for segment and partition problems.
Associate Research The general impression that purely functional languages do not allow side effects is
Fellow misleading. Instead, they dictate that effects must be introduced in a mathematically
manageable manner. One way to introduce e ects is through monads. Monadic programs
actually allow plenty of reasoning. We are studying their derivation, and also trying to
establish the conditions under which desired properties of one monadic effect can be
preserved in the presence of other monadic e ects.
II. Dependently Typed Programming
Based on the propositions-as-types principle, there have been type-theoretic foundations
and languages/systems in which the activity of proving mathematical theorems is
subsumed by programming with sophisticated types (called "dependent types"). Among
these approaches, there is an ambitious line of work on dependently typed programming
that aims to integrate full dependent types into conventional (in particular functional)
programming languages, guaranteeing program correctness while retaining natural
programming styles. A de ning characteristic of dependently typed programming is the use
of inductive families (and, recently, coinductive families too) to encode properties of interest
in datatypes such that the dependently typed programmer can implicitly establish and
exploit those properties while specifying computations on inhabitants of those datatypes.
Consequently, the programmer does not need to write explicit and separate proofs about
those properties, and can even get semantic hints in the form of type information during
program construction. We have conducted some successful preliminary experiments on
this new paradigm of blending programs and proofs, and are setting out to explore its full
potential.
134
實室 Programming Languages and Formal
驗
Research Laboratories Methods Laboratory
Research Faculty
Yu-Fang Chen / Chair The Programming Languages and Formal Methods research group develops techniques to
ensure program correctness. Our research into programming languages focuses on syntactic,
Research Fellow semantic, and pragmatic issues in the development of correct programs. Our work on formal
methods emphasizes the algorithmic, computational, and practical aspects of realistic program
Bow-Yaw Wang analyses. We apply mathematical and formal techniques to our investigations of research
problems. We also aim to develop tools and methodologies that can help developers write
Research Fellow code correctly.
Hsiang-Shang Ko I. Reasoning and Derivation of Functional and Monadic Programs
Assistant Research Purely functional languages, in which functions are true mathematical functions, offer
Fellow a simple model of computation in which programs can be understood as mathematical
equations whose properties can be proved using mathematical tools including induction.
Tyng-Ruey Chuang An e cient program can be derived from a program speci cation by stepwise equational
reasoning, whereby every step is justified by a theorem. This technique, called "program
Associate Research derivation", aims to provide formalization and patterns that help programmers to develop
Fellow programs and their correctness proofs at the same time. We have published some
interesting case studies of derivation, including approximation algorithms and algorithms
Shin-Cheng Mu for segment and partition problems.
Associate Research The general impression that purely functional languages do not allow side effects is
Fellow misleading. Instead, they dictate that effects must be introduced in a mathematically
manageable manner. One way to introduce e ects is through monads. Monadic programs
actually allow plenty of reasoning. We are studying their derivation, and also trying to
establish the conditions under which desired properties of one monadic effect can be
preserved in the presence of other monadic e ects.
II. Dependently Typed Programming
Based on the propositions-as-types principle, there have been type-theoretic foundations
and languages/systems in which the activity of proving mathematical theorems is
subsumed by programming with sophisticated types (called "dependent types"). Among
these approaches, there is an ambitious line of work on dependently typed programming
that aims to integrate full dependent types into conventional (in particular functional)
programming languages, guaranteeing program correctness while retaining natural
programming styles. A de ning characteristic of dependently typed programming is the use
of inductive families (and, recently, coinductive families too) to encode properties of interest
in datatypes such that the dependently typed programmer can implicitly establish and
exploit those properties while specifying computations on inhabitants of those datatypes.
Consequently, the programmer does not need to write explicit and separate proofs about
those properties, and can even get semantic hints in the form of type information during
program construction. We have conducted some successful preliminary experiments on
this new paradigm of blending programs and proofs, and are setting out to explore its full
potential.
134
