[Agda] AIM9

[KINOSHITA Yoshiki]

Dear all,

here is a tentative programt AIM9 meeting to be held in Sendai, Japan
from 27 Nov to 3 Dec.  We can still arrange a few more slots, so
please drop me a mail if you wish to give a talk.  For further
information, please watch

     http://unit.aist.go.jp/cvs/symposium/aim9.html

Best wishes,

Yoshiki.
------------------------------------------------------------------------
*****************************
**  AIM9 Program (tentative)
*****************************

------------------------------------------------------------------------
27 (Thu) November
* Talks and research seminars

 9:00       Opening

 9:15-10:00 Shin-Cheng Mu
            (Academia Sinica)
            "Algebra of Programming using Dependent Type."

            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.

10:00-10:45 Nils Anders Danielsson
            (The University of Nottingham)
            Title TBA

10:45-11:00 Break

11:00-11:45 Anton Setzer
            (Swansea University)
            Title TBA
11:45-12:30 Yoshinori Tanabe
            (The University of Tokyo)
            Title TBA

12:30-14:30 Lunch

14:30-15:15 Yoshifumi Yuasa
            (Tokyo Institute of Technology)
            Title TBA
15:15-16:00 Andreas Abel
            (Institute of Computer Science, Ludwig-Maximilians-University Munich)
            Title TBA

16:00-16:15 Break

16:15-17:00 Norio Kato
            (AIST)
            Title TBA
------------------------------------------------------------------------
28 (Fri) November
* Code sprint

 9:00       Tea/Coffee to get together
 9:30-10:30 Initial discussion and grouping for code sprint
10:30-12:00 Code sprint
12:00-14:00 Lunch
14:00-18:00 Code sprint
18:00-18:30 Daily progress report

19:30       Dinner at Sendai Plaza Hotel

------------------------------------------------------------------------
29 (Sat) November
* Excursion at Matsushima Archipelago

------------------------------------------------------------------------
30 (Sun) November
* Sendai sightseeing
* Dinner (local speciality)

------------------------------------------------------------------------
1 (Mon) December - 3 (Wed) December
* Code sprint

 9:00       Tea/Coffee to get together
 9:30-12:00 Code sprint
12:00-14:00 Lunch
14:00-18:00 Code sprint
18:00-18:30 Daily progress report

------------------------------------------------------------------------

--
Yoshiki Kinoshita, D.Sc.
Director
Research Center for Verification and Semantics (CVS)
National Institute of Advanced Industrial Science and Technology (AIST)
Mitsui-Sumitomo-Kaijo Senri Building 5F
1-2-14 Shin-Senri-Nishi-machi Toyonaka-shi
Osaka, 560-0083, Japan
Phone: 06-4863-5014  Fax: 06-4863-5052
E-mail: yoshiki at m.aist.go.jp
home page: http://staff.aist.go.jp/kinoshita.yoshiki/