[Agda] AIM9 program update

[KINOSHITA Yoshiki]

Dear all,

we have to update the program less than 24 hours after we sent you the
first version...  This is because we could not calculate the date and
time correctly and did not realise Andreas will reach Sendai in the
evening of 27 Nov.

We will probably not send to you the further change of the program, so
please continue to watch

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

the home page of AIM9.

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 <free talk slot>

16:00-16:15 Break

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

 9:00       Tea/Coffee to get together
 9:30-10:15 (free talk slot)
10:15-11:00 Andreas Abel (Ludwig-Maximilians-University Munich)
            Title TBA
11:00-11:15 Break
11:15-12:00 Initial discussion for Code Sprint (target setting, grouping, etc.)
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/