Time: 10:00-12:00, Nov. 26, 2008
Place: Lecture Room 1 (2005), 20F, National Institute of Informatics (map http://www.nii.ac.jp/introduce/access1-j.shtml)
Inquiry: Nobukazu Yoshioka (nobukazu_AT_nii.ac.jp)
Fee: Free
Programme:
– An international collaboration success story – A study on cost
etimation modeling method with German Franhofer IESE –
Yasushi Ishigai, Mitsubishi Research Institute, INC, Tokyo, Japan.
– Algebra of Programming using Dependent Types
Shin-Cheng Mu, Academia Sinica, Taiwan
Detailed information:
Title: An international collaboration success story – A study on cost
etimation modeling method with German Franhofer IESE –
Speaker:Yasushi Ishigai, Mitsubishi Research Institute, INC, Tokyo, Japan.
Abstract:
A success story in terms of international collaboration between German
Fraunhofer IESE and IPA/SEC on the study of cost estimation modeling. We
cooperatively applied “CoBRA” method to an industrial field and achieved
a good result. Also we submitted a paper to ICSE 2006, which was
successfuly accepted. I will talk about the background of the success
story as well as the method and the study.
Note: CoBRA (Cost estimation, Benchmarking, and Risk Assessment) is a
cost estimation modeling method developed at IESE.
Bibliography:
Yasushi Ishigai is Research Director of Research Center for Information
Technology at Mitsubishi Research Institute, INC, Tokyo, Japan. He is
also a part time researcher at Software Engineering Center of
Information technology Promotion Agency (IPA/SEC). He received a degree
in mechanical engineering (BSc and MSc) from the University of Tokyo,
Japan, in 1988.His research interest and industrial activities include
quantitative management, especially software cost modeling.
– – – – – – – – – – – – – – – – – – – – – – – – – – – – – – – – –
Title: Algebra of Programming using Dependent Types
Speaker: Shin-Cheng Mu, Academia Sinica, Taiwan
Abstract:
Relational program derivation is the technique of stepwise refining a
relational specification to a program by algebraic rules. The program
thus obtained is correct by construction. Meanwhile, dependent type
theory is rich enough to express various correctness properties to be
verified by the type checker.
We have developed a library, AoPA, to encode relational derivations in
the dependently typed programming language Agda. A program is coupled
with an algebraic derivation whose correctness is guaranteed by the type
system.
Two non-trivial examples are presented: an optimisation problem, and a
derivation of quicksort where well-founded recursion is used to model
terminating hylomorphisms in a language with inductive type.
Bibliography:
Shin-Cheng Mu is currently an assistant research fellow in Academia
Sinica, Taiwan. Before that he worked as a postdoc in the Programmable
Structured Document project in Information Processing Lab, University
of Tokyo during 2003 through 2006. He received his D.Phil from Oxford
University Computing Laboratory.
