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.
- 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 is closed.
There is no registration fee. Coffee breaks are included. Transportation, accommodation and meals are to be covered by the participant.
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.
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.
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
- rain gear / sun screen, depending on the weather
- swimsuit & towel, if you are up for an attempt at swimming.
|09:50||Meet at Central Station|
|10:10||Take tram #4, buss 76 to Rannebergen|
|12:30||Lunch, swimming? in Gäddevatten lake|
|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.
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).
|09.30||Session 1: Talks & Discussions|
|11.00||Session 2: Talks & Discussions|
We meet at Chalmers Teknikpark (+46 31 772 42 42) in room Apollo.
- 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).
|Tuesday, May 9|
|09.30||Andreas Abel: Eating your own dog food|
|10.15||Introduction, code sprint proposals, planning|
|11.15||Jesper Cockx: Modalities and polarities|
|Wednesday, May 10|
|09.30||Niels van der Weide: Higher Inductive Types in Programming|
|11.00||Andrea Vezzosi: Cubical Type Theory in Agda (demo code)|
|Thursday, May 11|
|09.30||Jonathan Prieto-Cubides: Proof Reconstruction in Classical Propositional Logic|
|11.00||Thierry Coquand: Partial type theory|
|19.00||Dinner @ Noba|
|Friday, May 12|
|09.30||Guillaume Allais: agdarsec - Total Parser Combinators|
|11:00||Peter Dybjer: Higher Inductive Types in the Grupoid Model|
|13.20||Anton Setzer: Programming GUIs with Agda|
|Saturday, May 13|
|09.30||Wolfram Kahl: (Re-)Creating Sharing in/for the GHC back-end of Agda|
|11.00||Fredrik Nordvall Forsberg: Variations on inductive-recursive definitions|
|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)|
|Sunday, May 14|
|19.00||Back in Gothenburg|
|Monday, May 15|
|09:30||Ulf Norell: Mystery Talk|
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.
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.
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.
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.
- 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
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/libraries. Just install it by running:
pip install agda-pkg
- 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.