AIMXVI

The sixteenth edition of the Agda Implementors’ Meeting: Theory, implementation, and applications of Agda.

Venue

AIM XVI takes place 3–9 October 2012 at IT University in Copenhagen (ITU). For accommodation ITU recommends a few places http://itu.dk/en/Forskning/For-konference-gaester/Accommodation.

Maps:

• A map of the ITU bulding
• An angle where we see the "Scrollbar" where the opening will be held

Daily Schedule (Draft)

09:30 - 11:00   Session 1: Talks & Tutorials
11:00 - 11:15 Coffee
11:15 - 12:00   Session 2: Talks & Discussions
12:00 - 13:00 Lunch
13:00 - 14:00 Break
14:00 - 15:30   Session 3: Code Sprints
15:30 - 16:00 Coffee
16:00 - 18:30   Session 4: Code Sprints
18:30 - 19:00   Wrap-up meeting: Results, Demos 
19:00 -       Leisure time

Program

(not etched in stone)

We, 03 Oct: 09:30 (Scrollbar) Opening, 
                              Towards A Higher Dimensional in Type Theory: The Case of Parametricity (by Jean-Philippe Bernardy)
                              Discussion of code-sprints
            13:00 (4A56)
Th, 04 Oct: 09:30 (2A52)      A practical Agda introduction (by Péter Diviánszky)
                              Copatterns: A new syntax for the definition of infinite things, like functions and objects defined by coinduction (by Andreas Abel).
Fr, 05 Oct: 09:30 (4A14)

Sa, 06 Oct: 09:30 (2A52)

Su, 07 Oct: 09:30 (2A52)
                          Notice that the building will probably be locked. But me (Daniel) will be present and be able
                          to open the door. My phone number is above so just send an sms.

                          The usual rotating doors will be totally closed so the ones you should use is the one on the side
                          facing the parking lot (i.e the opposite of the canal).

                          It seems that one rotating door (the one facing Kong Cafe) seems to be open.

            16:00 (Opera house) Some of us will attend the opera

Mo, 08 Oct: 09:30 (Scrollbar)  crypto-agda: Formalizing cryptography in Agda (by Nicolas Pouillard)
                               A syntax for bijections on bit vectors (by Daniel Gustafsson)
            13:00 (Multimedialab)
            14:00 (Designlab)

Tu, 09 Oct: 09:30 (Scrollbar)
            13:00 (2A52)
            Discussions and code-sprints; wrap-up meeting

Talks

• Copatterns: A new syntax for the definition of infinite things, like functions and objects defined by coinduction (by Andreas Abel).
• Towards A Higher Dimensional in Type Theory: The Case of Parametricity (by Jean-Philippe Bernardy)
• A practical Agda introduction (by Péter Diviánszky)
• crypto-agda: Formalizing cryptography in Agda (by Nicolas Pouillard)
• A syntax for bijections on bit vectors (by Daniel Gustafsson)

Code Sprints

• Copatterns in the Agda kernel (optional)
• Higher Dimensions for Parametricity
• Update Windows installer for Agda and D-Case/Agda (only Makoto Takeyama)
• Work towards allowing arbitrary local declarations, Work towards abolishing name equality (proposed by Makoto Takeyama)
• Liberate Agda from Emacs (web frontend for Agda, Péter Diviánszky)
• LaTeX-backend (see https://code.google.com/p/agda/issues/detail?id=697)
• Formalisation of "vague" concepts (Yoshiki Kinoshita)
• Formalisation of the catoid of setoids, and proving its basic properties (Yoshiki Kinoshita)

AIM XVI Code Sprint

Discussions and Code Sprint Suggestions

Participants

• Nicolas Pouillard
• Daniel Gustafsson
• Stephan Adelsberger
• Nils Anders Danielsson
• Steven Keuchel
• Andreas Abel
• Jean-Philippe Bernardy
• Guilhem Moulin
• James Chapman
• Yoshiki Kinoshita
• Makoto Takeyama
• Bengt Nordström
• Péter Diviánszky
• Ulf Norell
• Denis Firsov
• Maxime Beauquier

Slides

• Opening slides (practical information): http://wiki.portal.chalmers.se/agda/uploads/Main.AIMXVI/opening.html
• A practical Agda tutorial presentation: http://people.inf.elte.hu/divip/AgdaTutorial/About.html
• fun-universe: Tracking space and time through a restricted universe: https://nicolaspouillard.fr/publis/fun-universe-aim16.html
• A syntax for bijections on bit vectors: http://itu.dk/~dagu/AIMXVI.pdf

Excursion

Excursion will happen on Saturday, we will meet at the central station (facing Tivoli) at 09:30.

Google map of location of meeting

• The museum tour will be at Louisiana
• The walk will be at Stevns Klint
  We'll probably start by taking the train to Rødvig (København H 10:02-Køge 10:40, Køge 10:57-Rødvig 11:30). We might return from Store Heddinge (Store Heddinge H:55-Køge (H+1):21, Køge (H+1):26-København H ((H+2) mod 24):04, for 6 ≤ H ≤ 22).
  Information about the area. More information about the area (in Danish). map

Travel

We recommend you travel to Copenhagen Airport (Kastrup) for local transportation visit http://itu.dk/en/Forskning/For-konference-gaester/Transportation-.

Registration

Although no official registration is needed, we want to know how many will attend. If you want to give a talk please send us the title and an abstract.

To register, please send an email to (aim16 at ƛ.net -- or if you are not an unicode aficionado aim16 at xn--dia.net), filling out the following form:

Name:
Affiliation:
email:

Program:
* I'd like to give a talk or lead a discussion (yes/no):
Title:
Abstract: (optional)

* Suggestion for code-sprint (optional):