Page 38 - profile2014.indd

Programming Languages

and Formal Methods Lab

Lab

Research Faculty
Bow-Yaw Wang The Programming Languages and Formal Methods research group develops tech-
Research Fellow niques for ensuring program correctness. Our researches in programming languag-
es focus on the syntactic, semantic, and pragmatic issues in the development of
Yu-Fang Chen
Associate Research Fellow correct programs. The researches in formal methods emphasize on the algorithmic,
computational, practical aspects in the analysis of realistic programs. We apply
Tyng-Ruey Chuang mathematical and formal techniques in the investigation of our research problems.
Associate Research Fellow
We also aim to develop tools and methodologies to help developers writing correct
Shin-Cheng Mu codes.
Associate Research Fellow
Multi-core processors are now widely used in desktop computers, notebooks, and
even smart phones. Developers certainly would like to exploit concurrency to im-
prove the efficiency of applications. Yet concurrent programming is known to be
difficult. Even experienced developers may make mistakes in writing concurrent
programs. Subsequently, there are still a very limited number of concurrent pro-
grams despite of the prevalence of concurrent computer systems. In order to help
developers exploit the computational power in modern processors, the Program-
ming Languages and Formal Methods research group are currently working on lan-
guage and verification techniques for concurrent programs.

Type systems are widely deployed in modern programming languages to ensure
type safety. For example an ill-typed expression may add the number 0 to a charac-
ter ‘0’ and evaluate to an incorrect result. Type systems allow developers to identify
such type errors at the compile time. Concurrent programming is known to be er-
ror-prone, and the challenge of programmers is even made harder when a modern
program often consists of hundreds or even thousands of threads communicating
to each other. Modern programming languages adopt expressive type systems to
guarantee certain properties of programs.

“Session type” is a type system for message-passing concurrent programs that en-
sures that communication between threads follow certain protocol. More advanced
variations also guarantee deadlock-freeness. Some efforts were made to implement
session type systems by embedding them to existing languages. Those implement-
ed, however, are still far behind those existing on paper, due to inexpressiveness of
the type system in the host language. We plan to embed session type into Agda, a
language with an expressive dependent type system, hoping to build an integrated
environment in which programmers may program in Agda/Haskell, and use the type
system to guarantee correctness and termination.
We also plan to investigate the “proofs-as-programs” approach to program correct-
ness as embodied in proof assistants such as Coq and their program extraction
mechanisms, and to familiarize ourselves with the details of these tools so as to
understand their capacities and limitations. We have selected three application do-
mains to work on: 1) Derivatives of regular expressions, 2) Transformations of struc-
tural contents, and 3) Interactions of software components. The problems dealt with
in the above three domains can often be related to those encountered in general
application development. For example, Web application scripts shall process all user
inputs correctly (and avoiding common security pitfalls e.g. those caused by SQL

38 研究群 Research Laboratories