The sixteenth edition of the Agda Implementorsí Meeting: Theory, implementation, and applications of Agda.
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.
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
(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
- 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)
- 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)
Discussions and Code Sprint Suggestions
- 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
- 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 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
We recommend you travel to Copenhagen Airport (Kastrup) for local transportation visit http://itu.dk/en/Forskning/For-konference-gaester/Transportation-.
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):