The twenty-first Agda Implementors' Meeting will take place in Göteborg 2015-06-03 to 2015-06-09 (Wed to Tue). The meeting will be similar to previous ones:
* Presentations concerning theory, implementation, and
use cases of Agda.
* Discussions around issues of the Agda language.
* Plenty of time to work on or in Agda, in collaboration
with the other participants.
Important dates
- 2015-05-22
- Registration deadline
- 2015-06-03 to 2015-06-09
- AIM XXI
Note that if you want to stay at SGS Veckobostäder (see below) it may be wise to book a room as soon as possible.
Location
The meeting will be in Chalmers Teknikpark, which is a few minutes walking distance from Department of Computer Science and Engineering at Chalmers University of Technology (Campus Johanneberg). (A receptionist should be sitting by the entrance, and will be able to help you find your way.)
Lunch and coffee breaks will be provided, as well as WIFI through eduroam.
Saturday 6th the meeting will be in the lunch room of the department
From the central train station, you can go to Chalmers by public transportation:
- Tram 7 with direction Tynnered
- Tram 13 with direction Sahlgrenska via Skånegatan
- Bus 58 with direction Brottkärr
You can also go to Chalmers from the transportation hub Brunnsparken, a few minutes walk from the central station:
- Tram 7 with direction Tynnered
- Tram 10 with direction Guldheden
- Bus 16 with direction Högsbohöjd
- Bus 19 with direction Fredriksdal or Bifrost (get off at Chalmers Tvärgata)
- Bus 58 with direction Brottkärr
A short walk from the tram stop at Chalmers will take you to the venue Chalmers Teknikpark for the meeting.
Excursion
Sunday 7th: Walking on the Bohusleden, stage 3 from Kåsjön to Skatås. Bring:
- outdoor shoes
- water
- lunch
- rain gear / sun screen, depending on the weather
- swimsuit & towel, if you are up to swimming in Härlanda tjärn
09:50 Meet at Korsvägen 10:07 Bus 513 to Kåsjön 10:27 Start hiking! ... hiking ... lunch ... swimming? ... coffee ... 18:00 We should be done.
Rough time estimate: Hiking (3 hours), breaks (2 hours), coffee (1 hour), trip back (1 hour). Café Skatåsmålet, Olbersgatan, 41655 Göteborg, tel: +46-31-250840, or Torps Café, Kyrkåsgatan 13, 41656 Göteborg, tel: +46-31-254360.
Dinner
Monday, 8 June, 7pm, at the http://www.flyingbarrel.se/, partially sponsored by https://www.fireeye.de/ Dresden.
Daily Schedule
09:30 - 11:00 Session 1: Talks & Tutorials 10:45 - 11:15 Coffee 11:00 - 12:30 Session 2: Talks & Discussions 12:30 - 13:30 Lunch 13:30 - 15:00 Session 3: Code Sprints 15:00 - 15:30 Coffee 15:30 - 17:30 Session 4: Code Sprints 17:30 - 18:00 Wrap-up meeting: Results, Demos
We meet at Chalmers Teknikpark (+46 31 772 42 42) in room Apollo/Artemis.
Exceptions:
- Thursday afternoon we meet in FL52 (Fysikhuset, Chalmers campus).
- Saturday we meet in the Chalmers lunchroom (floor 8 of EDIT building).
Program
(not etched in stone)
Wed, June 03 09:30 Andreas Abel: 10 years of Agda2 10:25 Personal introductions and sprint suggestions 11:00 Coffee 11:30 Anton Setzer, Karim Kanso's PhD thesis integrating model checking and SAT into Agda 12:00 Anton Setzer, How to Reason Informally Coinductively 12:30 Lunch Thu, June 04 [EARLY START!] 09:00 Jesper Cockx, Unification in a context of postponed equations 09:45 Ulf Norell, Reflections about reflection 10:30 Coffee 11:00 Nicolas Pouillard, Programming with linear types, a tutorial 12:00 Lunch MOVE to FL52 for the afternoon. Fri, June 05 09:30 Anders Mörtberg, An Implementation of a Cubical Type Theory 10:15 Bas Spitters, Cubical sets as a classifying topos 11:00 Coffee 11:30 Peter Dybjer, Implementing Martin-Löf's meaning explanations in Agda 12:30 Lunch Sat, June 06 10:00 Meet at EDIT main entrance. The door will be closed, so call +460728504642 (Andrea) to let you in if you arrive later Then: Hacking in Chalmers EDIT lunchroom Sun, June 07 09:50 Excursion (Korsvägen!) Mon, June 08 09:30 Thorsten Altenkirch, Type Theory eats itself --- without indigestion (joint work with Ambrus Kaposi) 10:15 Coffee 10:45 Christoph-Simon Senjak, An Implementation of Deflate in Coq 11:30 Keiko Nakata, Formal verification at FireEye 12:30 Lunch 19:00 Dinner at the Flying Barrel Tue, June 09 09:30 Code sprints
Travel to Göteborg
Local airports: Landvetter.
Göteborg is served by trains by SJ. For information how to get here from overseas, see for instance The Man in Seat Sixty-One... and Deutsche Bahn.
Accommodation
You may want to use SGS Veckobostäder (350 SEK/night for a single room if you stay for 8 nights). There are many other options.
Registration
You register for the meeting by filling out this form
There is a fee of 1000kr (~106 EUR) which you can pay here.
Participants
Andreas Abel, Gothenburg University (co-organizer) +49-179-40033323
Stephan Adelsberger, WU Wien
Guillaume Allais, Strathclyde U
Thorsten Altenkirch, Nottingham (invited speaker)
Guillaume Brunerie, Nice
Ana Bove, Chalmers
James Chapman, IoC Tallinn
Jesper Cockx, KU Leuven
Nils Anders Danielsson, Chalmers
Peter Dybjer, Chalmers
Hans Bugge Grathwohl, Aarhus U
Pepijn Kokke, Utrecht U
Yoshiki Kinoshita, Kanagawa U
Paul Laforgue, Lille University
Victor Lopez Juan, Chalmers
Guilhem Moulin, Chalmers
Keiko Nakata, FireEye Dresden (invited speaker)
Bengt Nordström, Chalmers (co-organizer)
Ulf Norell, Chalmers
Nicolas Pouillard, Copenhagen
Christoph-Simon Senjak, LMU München
Anton Setzer, Swansea U (invited speaker)
Bas Spitters, Aarhus U
Makoto Takeyama, Kanagawa U
Andrea Vezzosi, Chalmers (co-organizer) +46-72-6504642
Matthew Wilson, Formal Solutions
Theo Winterhalter, ENS Cachan
Talks
Andreas Abel, 10 Years of Agda2
Anton Setzer, How to Reason Informally Coinductively. PhD Thesis, source code and MRes thesis by Karim Kanso
Jesper Cockx, Unification in a context of postponed equations (Slides).
Nicolas Pouillard, Programming with Linear Types, a tutorial (Slides, Tutorial).
Anders Mörtberg, An Implementation of a Cubical Type Theory (Slides).
Peter Dybjer, Implementing Martin-Löf's Meaning Explanations in Agda (Agda-files).
Christoph-Simon Senjak, An Implementation of Deflate in Coq.
Ulf Norell, Reflections on Reflection.
Jesper Cockx, Unification in a context of postponed equations
Agda's algorithm for checking definitions by dependent pattern matching relies a great deal on unification. On the one hand, we want this unification algorithm to be as powerful as possible, in order to accept more definitions. On the other hand, there is a desire to be conservative with respect to the standard axioms of type theory. One area of tension between these two desires is the postponing of equations. The theory doesn't say anything about it, yet the implementation happily postpones any equation they can't solve right away. That this leads to problems, can be seen in issues both old (Issue 292) and new (Issue 1406, 1435). In an attempt to fix these problems, forcing rules were added, allowing Agda to skip unification of certain arguments when they must be equal because of the type. However, the current implementation doesn't have enough information available to make a correct decision when to apply forcing, leading to other problems (Issue 1427).
Rather than restrict the current postponing mechanism to avoid these problems, I propose to rebuild unification up from the foundations with postponed equations in mind. The central idea to do this is to keep track of how the type of each equation depends on which previously postponed equations. This is done by introducing a new variable for each postponed equation, serving as a placeholder for the solution of that equation until it is solved. It turns out that having this context of postponed equation actually allows us to apply more unification rules, giving us a solution where previously there was none. To take advantage of this benefit, I introduce the idea of reverse unification rules, which can introduce new postponed equations or combine them when this is useful. It turns out that these reverse unification rules subsume the rules for skipping unification of forced constructor arguments.
In my presentation, I will delve into some examples where postponed equations are useful, and also some examples of what goes wrong when it is implemented naively. After that, I will discuss my proposal how to handle postponed equations in general: first, the beautiful theory of working in a context of postponed equations, then the complex art of applying reverse unification rules to bring these postponed equations in just the right form, and finally the ugly practice of implementing all of this.
Thorsten Altenkirch, Type Theory eats itself --- without indigestion (joint work with Frederik Forsberg and Ambrus Kaposi)
Implementing a total syntax for a language with dependent type incurred a huge overhead due to having to be explicit about families of setoids etc. We propose to use first order Higher Inductive Types with we call QITs (Quotient Inductive Types). They already play an important role when formalizing infinitary algebraic theory like the Cauchy Reals in the HoTT book. A simple example is given by infinitely branching trees quotiented by permutation. The definition using quotient is unsatisfactory because we cannot lift the node constructor without using countable choice. A similar problem has recently been observed in the context of the partiality monad by Uustalu et al.
As far as TT in TT is concerned we have formalized a basic type theory with recursor and eliminator and have implemented the set-theoretic semantics using the recursor. The formalisation of the logical predicate translation and the presheaf interpretation is work in progress. The latter would lead to NBE which requires a definition of normal forms. However, it turns out that the definition of normal forms already requires normalisation. Also we observe that you need truncation or UIP to define normal forms.