Call for Participation
Agda Implementors Meeting XI

The Agda Implementors Meetings have been held twice a year in principle since 2004. The AIM meetings are really "Agda Users and Implementors Meetings," that is, meetings where Agda users and implementors get together and exchange ideas, write Agda code, while simultaneously implementors work on modifications of the Agda system.

The AIM meeting usually consists of talks and code sprint sessions. Talks are invited by the organiser, and all participants are expected to propose his/her own project for a code sprint session.

At the start of AIM, the participants get together and are expected to participate in projects they wish to take a part in. Then it is discussed which project to start. A short meeting is held at the end of every day so that each project reports its progress. A longer meeting is held at the end of the whole AIM to summarize the result and future of the project.

Everyone who is seriously interested in Agda, not only implementors but those who are willing to write code in Agda or documentation about Agda is welcome to the meeting. They are expected to make a constructive contribution to the code sprint.

Important Dates:

  Hotel registration (reduced rate):    (Tue) 23 February, 2010
  Participation registration:           (Fri) 12 March, 2010
  Meeting:                              (Wed) 24 - (Tue) 30 March, 2010

Meeting Date: (Wed) 24 - (Tue) 30 March, 2010

Deadline of participation registration: (Fri) 12 March, 2010.

Venue: Awaji Yumebutai International Conference Centre

Access to Awaji:

Some advice to people who arrive by international flights:

Closest international airport is Kansai International Airport (KIX). From Kansai airport, take a limousine bus to Sannomiya Station, change to a local bus to Awaji Yumebutai, as depicted in the above URL.

Alternatively, you can land at Narita International Airport (NRT) near Tokyo or Central Japan International Airport (NGO) near Nagoya; in that case, find the way by yourself from either airport to Sannnomiya Station, then follow the above instruction. Send any inquiries to .

WARNING: Please be advised to change the currency before arriving at the conference centre; probably at the airport or in a large city like Osaka, Kobe or Tokyo. The conference centre is not in town and there are no banks or post offices nearby where one can exchange currency.


Participants are requested to make TWO registrations: one for the meeting and the other for the hotel.

Hotel registration

Awaji Westin Hotel is located next to the conference center and we have tentative booking for 40 persons. We recommend participants to stay in the hotel, as the area is rather rural and there are no other accommodations within at least 1km from the conference center. Moreover, the public transportation is not frequent.

The participants are expected to contact Awaji Westin Hotel directly, notifying that he/she is to attend AIM XI meeting by filling the application form attached to this message and sending it to before 23 February, 2010. Early registration is recommended as the number of the hotel rooms are limited.

The special rate of Awaji Westin Hotel ( for the conference participants is:

13,500 JPY (Yen) per night, including breakfast, service charge and tax.

Meeting registration

To register for the meeting, send the Meeting Registration Form attached to this message to before Friday 12 March, 2010.

The registration fee is the following, and will be collected on site at the reception by JPY (Yen).

Excursion: Himeji castle.

An excursion to Himeji castle and dinner is planned on Saturday, 27 March. It costs 7,000 yen per person, as written above. The main tower of the castle was built in 16th century, and is now a Japan's national treasure as well as one of world heritage. Because of its beautiful white main tower, it is also called the "heron castle." After April 2010, we cannot see its whole figure for several years because of a big maintainance work.

URL of Himeji castle:

Cultural experience: Tea ceremony.

The conference centre has a special room for tea ceremony, designed by Tadao Ando, one of the leading contemporary architects who also designed the buildings of the whole area. We invite a master of tea ceremony and enjoy Japanese traditional tea ceremony with 'ousu' (meaning 'thin tea' although it is much stronger than English tea!) and Japanese sweet. It costs 4,000 yen per person.

AIM XI Program :

  (Wed) 24 March
   9:30 coffee and tea
  10:00 talk 1  Thorsten Altenkirch
                PiSigma - a core language for Agda?
  11:00 organisation of code sprint 1
  12:00 lunch
  14:00 talk 2  Makoto Takeyama
                Assurance Cases in Agda
  15:00 coffee and tea
  15:30 talk 3  Nils Danielsson
                Operational Semantics Using the Partiality Monad
  16:30 talk 4  Shunsuke Yatabe
                Specification check tool S3
  17:00 organisation of code sprint 2
  18:00 supper

  (Thu) 25 March
   9:00 talk 5  Andreas Abel
                On Irrelevance and Extraction in Type Theory
  10:00 coffee and tea
  10:30 talk 5  Norio Kato
                Title TBA
  12:00 lunch
  14:00 code sprint
  15:30 coffee and tea
  17:00 wrap-up meeting
  18:00 Supper

  (Fri) 26 March
   9:00 coffee and tea
   9:30 code sprint
  12:00 lunch
  14:00 code sprint
  15:30 coffee and tea
  17:00 wrap-up meeting
  18:00 Supper

  (Sat) 27 March
   9:00 outing
  18:00 Dinner at Sannomiya, city centre of Kobe  

  (Sun) 28 March
  14:00 cultural experience

  (Mon) 29 March
   9:00 coffee and tea
   9:30 code sprint
  12:00 lunch
  14:00 code sprint
  15:30 coffee and tea
  17:00 wrap-up meeting
  18:00 Supper

  (Tue) 30 March
   9:00 coffee and tea
   9:30 code sprint
  12:00 lunch
  14:00 overall wrap-up meeting
  15:30 coffee and tea
  16:30 end of the workshop


Research Center for Verification and Semantics (CVS),
National Institute of Advanced Industrial Science and Technology (AIST)

Send inquiries to


       AIM11(Agda Implementor's Meeting)HOTEL REGISTRATION FORM

Fill and send this form to
before 23 February
to get the Special Rate (Breakfast and Tax included) of
Single:      13,500 JPY per room
TWIN/Double: 18,000 JPY per room (9,000 JPY per person)
TRILLE:      22,500 JPY per room (7,500 JPY per person)

* cancellation made within 7 day prior to your arrival will be subject
  to the applicable charge
* Check-in: 3:00 p.m.,  Check-out: 11:00 a.m.
* Please note that there is no Bank or ATM in the hotel, although you
  can make a payment to the hotel with a credit card.
* Be advised to exchange your money at the airport.

Title:  (retain the appropriate)  Prof.  Dr.  Mr.  Ms.

First Name:
Middle Name:
Family Name:


E-mail address:



Room Type: (retain the appropriate)
     1 person Single
     2 persons Twin
     2 persons Double
     3 person Triple

Check-in Date:

Check-out Date:

Comment (Names of Room Partners, Non-Smoking request, etc.):


                      MEETING REGISTRATION FORM
    Fill and send this form to before 12 March

Given Name:
Middle Name:
Family Name:


E-mail address:

Your Dietary Condition:

Participation to Excursion and Dinner:  YES / NO

Participation to Cultural Experience:   YES / NO

Your Experience with Agda and other proof assistants:

Your proposal of Code Sprint / Documentation Sprint:


Related Events:

FLOPS 2010:
Tenth International Symposium on Functional and Logic Programming April 19-21, 2010 Sendai, Japan