The twenty-fifth Agda Implementors' Meeting will take place in Gothenburg, Sweden from 2017-05-09 to 2017-05-15 (Tue to Mon). 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
- 2017-04-30
- Registration closed.
Talk proposals: If you didn't give a talk title when you registered, you can use the talk proposal form.
- 2017-05-09 (Tu) to 2017-05-15 (Mo)
- AIM XXV
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.
Registration
Registration is closed.
There is no registration fee. Coffee breaks are included. Transportation, accommodation and meals are to be covered by the participant.
Talks
Presentations on theory, implementation, and use cases of Agda and type theory are welcome.
If you would like to present something, you can propose a talk either when you register, or, if you are have already done so, by using the talk proposal form.
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). Look for room Apollon. A receptionist should be sitting by the entrance, and will be able to help you find your way.
Friday 12th and Monday 15th the meeting will be in the Chalmers Conference Center, which is in front of the Chalmers tram stop. Look for room Valdemar or Ledningsrummet on the second floor.
Saturday 13th 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 14th May: Walking on the Bohusleden from Rannebergen to Bohusfästning (11 km). Bring:
- Västtrafik card with >55 kr saldo. Alternatively, you can buy tickets for the bus and tram with a credit card.
- comfortable shoes
- water
- lunch!
- rain gear / sun screen, depending on the weather
- swimsuit & towel, if you are up for an attempt at swimming.
| Daily schedule | |
|---|---|
| 09:50 | Meet at Central Station |
| 10:10 | Take tram #4, buss 76 to Rannebergen |
| 10:45 | Hike! |
| 12:30 | Lunch, swimming? in Gäddevatten lake |
| 13:30 | Continue hiking |
| 14:30 | Break (~½ hour) |
| 16:00 | Reach Bohus fortress, tour around Kungälv |
| 18:00 | Take Grön Express back to Gothenburg |
Once in Kungälv, you can walk around Bohus fortress, check out the old city center, and have coffee. There are buses back to Gothenburg every 15 min until late.
If you do not want to hike, you can spend the afternoon in Kungälv, and wait for us there. The Bohus fortress is open for visits from 11am to 4pm. There is a small nature reserve nearby, Fontin.
Dinner
Those who want to can join for dinner Thursday, 11th May, 7pm, at NOBA Nordic Bar. Located at Viktoriagatan 1a, menu (250 - 380 SEK pp).
We are many people, so we will need to choose the food in advance. A sheet will be available on Tuesday if you want to sign up. If you didn't have a chance to sign up on Tuesday, ask Víctor as soon as possible.
We will meet at the venue 6:20 and walk from there (~25 minute walk, downhill). If you don't want to walk, you can take tram 7 (direction Bergsjön) or 10 (direction Biskopsgården) and get off at Vasaplatsen (2 stops). Tickets can be bought with card only on the onboard machine. You want a Gothenburg adult ticket (29 kr).
Daily Schedule
| Daily schedule | |
|---|---|
| 09.30 | Session 1: Talks & Discussions |
| 10.30 | Coffee break |
| 11.00 | Session 2: Talks & Discussions |
| 12.00 | Lunch |
| 13.15 | Code sprints |
| 15.00 | Coffee break |
| 15.30 | Code sprints |
| 17.30 | Wrap-up meeting |
We meet at Chalmers Teknikpark (+46 31 772 42 42) in room Apollo.
Exceptions:
- Friday and Monday we meet at Chalmers Konferenscenter, room Valdemar-Ledningsrummet. 1 floor upstairs. (in front of the Chalmers tramstop).
- Saturday we meet in the Chalmers lunchroom (floor 8 of EDIT building, Rännvägen 6b). We meet at the building entrance before 9.30! In case of any issues phone Víctor (+46 705 75 42 36).
Program
| Tuesday, May 9 | |
|---|---|
| 09.30 | Andreas Abel: Eating your own dog food |
| 10.15 | Introduction, code sprint proposals, planning |
| 10.45 | Coffee break |
| 11.15 | Jesper Cockx: Modalities and polarities |
| 12.00 | Lunch |
| 13.15 | Code sprints |
| 15.00 | Coffee break |
| 15.30 | Code sprints |
| 17.30 | Wrap-up meeting |
| Wednesday, May 10 | |
| 09.30 | Niels van der Weide: Higher Inductive Types in Programming |
| 10.30 | Coffee break |
| 11.00 | Andrea Vezzosi: Cubical Type Theory in Agda (demo code) |
| 12.00 | Lunch |
| 13.15 | Code sprints |
| 15.00 | Coffee break |
| 15.30 | Code sprints |
| 17.30 | Wrap-up meeting |
| Thursday, May 11 | |
| 09.30 | Jonathan Prieto-Cubides: Proof Reconstruction in Classical Propositional Logic |
| 10.30 | Coffee break |
| 11.00 | Thierry Coquand: Partial type theory |
| 12.00 | Lunch |
| 13.15 | Code sprints |
| 15.00 | Coffee break |
| 15.30 | Code sprints |
| 17.30 | Wrap-up meeting |
| 19.00 | Dinner @ Noba |
| Friday, May 12 | |
| 09.30 | Guillaume Allais: agdarsec - Total Parser Combinators |
| 10.30 | Coffee break |
| 11:00 | Peter Dybjer: Higher Inductive Types in the Grupoid Model |
| 12.00 | Lunch |
| 13.20 | Anton Setzer: Programming GUIs with Agda |
| 14.20 | Code sprints |
| 15.00 | Coffee break |
| 15.30 | Code sprints |
| 17.30 | Wrap-up meeting |
| Saturday, May 13 | |
| 09.30 | Wolfram Kahl: (Re-)Creating Sharing in/for the GHC back-end of Agda |
| 10:30 | Coffee break |
| 11.00 | Fredrik Nordvall Forsberg: Variations on inductive-recursive definitions |
| 12.00 | Lunch |
| 13.30 | Code-sprints |
| 15.00 | Coffee break |
| 15.30 | Víctor López Juan: How to write documentation (tutorial) |
| 16.00 | Jonathan Prieto-Cubides: A purpose of a package manager for Agda (demo) |
| 16.30 | Code-sprints |
| 17.30 | Wrap-up meeting |
| Sunday, May 14 | |
| 10.00 | Excursion |
| 19.00 | Back in Gothenburg |
| Monday, May 15 | |
| 09:30 | Ulf Norell: Mystery Talk |
| 10:30 | Coffee break |
| 11:00 | Code sprints |
| 12.00 | Lunch |
| 13.15 | Code sprints |
| 15.00 | Coffee break |
| 17.30 | Wrap-up meeting |
Travel to Göteborg
Local airport: Landvetter. There is an airport shuttle operated by Flygbussarna that takes you to the city center. You can buy tickets online at a small discount, or on board with a credit card. A ticket local transport for 90 minutes is included in the shuttle ticket. Make sure to ask the bus driver for it before you leave the bus.
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.
Travel inside Gothenburg
All local transport inside Gothenburg is managed by Västtrafik and its subcontractors. On trams, you can buy single tickets with a credit card on board for 29kr. You cannot buy tickets onboard buses. All tickets are valid on all trams, (blue) buses and ferries inside Gothenburg for 90 minutes.
Tickets can also be purchased at 7-Eleven and Pressbyrån. If you plan to travel daily, you can buy a reloadable card for 50 kr deposit + 100 kr minimum top-up. Each trip inside the city with a reloadable cost of 26 kr. The deposit is used to cover the cost of a trip when there is not enough money on the card. It is possible for two or more of people to travel on the same card. Ask a local to help you use the card reader.
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 no registration fee. Transportation, accommodation, and meals are to be covered by the participant.
Amenities
Coffee breaks will be provided, as well as WiFi. If you don't have access to 'eduroam', ask Víctor for a temporary user and password.
Meals are not covered. There are many options for lunch around campus; for example:
- Restaurang Einstein. Same building as the meeting, 85 SEK.
- Student Union Restaurant. 80 SEK.
- Mook Thai Restaurant. Up the hill. Starting 79 SEK.
- Alpa Baguetteria. Engedahlsgatan 6 (5 min walk). 40 SEK.
- Sushi Me. Gibraltargatan (5min). Around 75 SEK.
- Yoko Sushi. Gibraltargatan (5min). Around 75 SEK.
Participants
- Jesper Cockx, KU Leuven
- Víctor López Juan, Chalmers (main organizer). Tel: +46 705 75 42 36.
- Andrea Vezzosi, Chalmers
- Mike Koel, Minneapolis
- Kristen VerSteeg, Minneapolis
- John Leo, Bellevue, Washington
- Stephan Adelsberger, Vienna University of Economy
- Andreas Abel, Gothenburg University
- Peter Dybjer, Chalmers
- Siavash Hamedani, Chalmers
- Ulf Norell, Gothenburg University
- Nils Anders Danielsson, Gothenburg University
- Paul Gustafsson, Texas A&M University, TX, USA
- Youyou Cong, Ochanomizu University
- Christian Sattler, University of Gothenburg
- Wolfram Kahl, McMaster University, Hamilton, ON, Canada
- Gleb Lobanov, Chalmers
- Fredrik Nordvall Forsberg, University of Strathclyde, Glasgow
- Jonathan Prieto-Cubides, EAFIT University, Medellín
- Thierry Coquand, Gothenburg University
- Niels van der Weide, Radboud University, Nijmegen
- Guillaume Allais, Radboud University Nijmegen
- Anton Setzer, Swansea University, UK
- Simon Huber, University of Gothenburg
- Konstantinos Brilakis, Chalmers
- Yoshiki Kinoshita, Kanagawa University
Talks
Andreas Abel: Eat your own dog food
Remarks on the Agda development process.
Ulf Norell: Mystery Talk (code)
Inline, correct by construction, X86_64 assembly programming in Agda.
Peter Dybjer: Higher Inductive Types in the Groupoid Model
Wolfram Kahl: (Re-)Creating Sharing in/for the GHC back-end of Agda
Fredrik Nordvall Forsberg: Variations on inductive-recursive definitions
Inductive-recursive definitions allows the simultaneous construction of a family (U : Set, T : U -> D) where U : Set is inductively defined and the function T : U -> D is recursively defined for some (possibly large) type D. The prototypical example of an inductive-recursve definition is Martin-Löf's universe a la Tarski.
Dybjer and Setzer gave an axiomatisation of inductive-recursive definitions by exhibiting them as initial algebras of certain functors between families Fam D -> Fam E. The question of composition of DS-definable functors arises naturally: given two DS-definable functors F : Fam C -> Fam D and G : Fam D -> Fam E, is their composition G . F : Fam C -> Fam E DS-definable? Perhaps surprisingly, the answer seems to be no. I will present two alternative axiomatisations of inductive-recursive definitions: one is a subsystem of "uniform" definitions, and the other a supersystem with a dependent product constructor added. Both of these systems are closed under composition.
(This is joint work with Neil Ghani, Conor McBride and Stephan Spahn.)
Jesper Cockx: Modalities and polarities (slides)
The future of annotations on function spaces in Agda.
Jonathan Prieto-Cubides: Proof Reconstruction in Classical Propositional Logic (slides)
We reconstruct using Agda and Athena Classical Propositional Logic proofs generated by Metis prover. Our long term goal is to develop a SledgeHammer like-tool for Agda.
Niels van der Weide: Higher Inductive Types in Programming
We discuss some examples of higher inductive types with applications in programming. Examples might include natural numbers modulo n, lists, finite sets, expressions with + and natural numbers, and maybe more.
Guillaume Allais: agdarsec - Total Parser Combinators
Anton Setzer: Programming GUIs with Agda (Slides)
This is joint work with Andreas Abel and Stephan Adelsberger. We will show how to program with GUIs in Agda using action listeners and a combination of client-side and server side programming. This research has been written up in our article Andreas Abel, Stephan Adelsberger, Anton Setzer: Interactive Programming in Agda - Objects and Graphical User Interfaces, http://www.cs.swan.ac.uk/~csetzer/articles/ooAgda.pdf with agda code available at https://github.com/agda/ooAgda
Thierry Coquand: Partial type theory
Agda can be presented as the total subset of a partial type theory. We describe a (typed) denotational semantics of partial type theory, and use it to prove, in a proof-theoretically weak metatheory, subject reduction and the fact that two convertible terms have the same Bohm tree.
Andrea Vezzosi: Cubical Type Theory in Agda
Jonathan Prieto-Cubides: [ Agda-Pkg ] A package manager for Agda (demo)
The Agda package manager that we all have been waiting for. This tool does not
modify Agda at all, it will just manage systematically the directory .agda and
its files: .agda/defaults and .agda/libraries. Just install it by running:
pip install agda-pkg
Code sprints
- New test suite for the specification (both successful and failure cases) AA
- New semantics for record declarations (with interleaved fields and defs) AA
- Experiments with explicit substitutions UN
- Small projects HITs in Agda NvdW
- A look at auto GA
- Serializing warnings FNF
- Documentation on literate Agda for Beamer presentations JL
- GHC backend improvements Issue 1895 WK
- Fix current alt-consistency issues (!) in Agda JC
- Modality annotations on fun. spaces JC
- Documentation on the cubical backend PG, TC
- Feature: Flag to show libraries being used JPC
- (Named) default arguments in Agda (a la Python or OCaml) AS (example using instance arguments)
- Add lagda-lite literate backend AS
- Working with components in Agda AS
Wrap-up meeting summary
A short summary of the daily progress can be found here.