The twenty-eighth Agda Implementors' Meeting will be held in Nottingham, United Kingdom at the university's school of computer science from 15 Oct 2018 to 20 Oct 2018 (Monday to Saturday). The plan is to have:
- Talks and presentations about the theory, implementation, and use cases of Agda.
- Many discussions about Agda, including potential new features, goals, milestones.
- Plenty of time to work on or in Agda, in collaboration with the other participants.
Important dates
- 2018-10-10
- Registration deadline
The deadline is soft, and if you miss it, you will still be very welcome to come. However, it will be helpful for planning if you let Nicolai know that you intend to come. A short email is enough; of course, you can still make suggestions afterwards.
- 2018-10-15 (Mon) to 2018-10-20 (Sat)
- AIM XXVIII
Caveats
Visa
Britain is NOT in the Schengen area! If you have an EU passport/ID card, this is not a problem (at least until early next year and hopefully afterwards); otherwise, you might need an additional visa. Please contact Nicolai if you need help.
Power adaptor
Britain does not have the Euro power plug, so remember to bring your power adaptor! (Or learn how to push a (slim) Euro plug into a UK socket! :))
Registration
Please register for this meeting by filling out the form below and sending it to Nicolai.
There is no registration fee. Coffee breaks may be included (probably they are). Transportation, accommodation and meals are to be covered by the participant. There will (probably) be an excursion which may cause additional costs for the participants as well (details to be determined).
Registration form
Agda Implementors' Meeting XXVIII
Name:
Title and optionally abstract (if you want to give a talk or lead a discussion; optional):
Suggestions for code sprints (optional):
Additional comments (optional):
Participants
- Gun Pinyo
- John Leo
- Thorsten Altenkirch
- Paolo Capriotti
- Jakob von Raumer
- Filippo Sestini
- Nicolai Kraus
- Jesper Cockx
- Matthew Daggitt
- Niels van der Weide
- Andreas Abel
- Nils Anders Danielsson
- Ulf Norell
- Andrea Vezzosi
- András Kovács
- Péter Diviánszky
- Niccolò Veltri
- Fredrik Nordvall Forsberg
- Guillaume Allais
- Adam Oliver
- Ben Price
- Alexander McKenna
- Anton Setzer
- ... your name could be here :)
Daily Schedule (important parts)
Sunday (14/10)
Evening, from 7pm: We meet in the pub **Rose and Crown**. Address: 500 Derby Road, Lenton, NG7 2GW, just at the southern exit of Jubilee Campus. The pub serves food until 9pm.
Monday (15/10)
Start: 9:30, location: room C1 of Computer Science, Jubilee Campus. Breaks: coffee, tea, biscuits will be served at 10:00 and 15:30, lunch in Aspire at 12:00.
Tuesday (16/10)
Start: 9:30, location: room C1 of Computer Science, Jubilee Campus. Breaks: coffee, tea, biscuits will be served at 10:30 and 15:30, lunch in Aspire at 12:00.
Wednesday (17/10) - Excursion
The train leaves at 9:47 from Nottingham train station. Meeting time: 9:20 in the entrance hall (we will go to the platform no later than 9:35, and if you arrive later it could become difficult to get through the ticket barriers since the group ticket will already be at the platform). The plan is as follows:
- 9:47 - 11:39 by train to Hope
- 13:00 - 14:00 lunch in Castleton
- after lunch: continue the hike like 8 years ago, but reversed: Castleton-Lose Hill-Great Ridge-Hollins Cross-Edale
- 17:30 - 19:20 pub and dinner in Edale
- 19:32 - 21:34 bus and train back to Nottingham
Thursday (18/10) to Saturday (20/10)
Regular meeting days, similar to Monday and Tuesday with the difference that coffee/tea/biscuits/fruit/juice will be served at 9:30 and 13:00 (so that we have coffee right at the beginning and directly after lunch).
Detailed program (suggestion, flexible)
| Sunday, 14 Oct | |
|---|---|
| 19:00 | Rose and Crown pub |
| Monday, 15 Oct | |
| 09:30 | Introduction & planning |
| 10:00 | Coffee break |
| 10:30 | Thorsten: Coherent (intrinsic) type theory |
| 12:00 | Lunch |
| 13:00 | Groups/Code sprints/Discussions |
| 15:30 | Coffee break |
| 16:30 | Groups/Code sprints/Discussions |
| 17:45 | Wrap-up meeting |
| Tuesday, 16 Oct | |
| 09:30 | Niels: Eliminating Traversals in Agda (Agda code on GitHub) |
| 10:30 | Coffee break |
| 11:00 | András: Constructing Quotient Inductive-Inductive Types |
| 12:00 | Lunch |
| 13:00 | Groups/Code sprints/Discussions |
| 15:30 | Coffee break |
| 16:30 | Groups/Code sprints/Discussions |
| 17:30 | Wrap-up meeting |
| Wednesday, 17 Oct - EXCURSION to Peak District | |
| For details, see the section above! #-times are sharp | |
| 9:20 | Meeting at Nott station main entrance hall |
| #9:47 | Train to Hope (via Sheffield) |
| 13:00 | Lunch in Castleton |
| Walk like 8 years ago, but reversed | |
| 17:30 | Pub and Dinner in Edale |
| #19:32 | Train to Nottingham |
| 21:34 | Arrival in Nottingham |
| Thursday, 18 Oct | |
| 09:30 | Nisse: Total Definitional Interpreters for Time and Space Complexity |
| 10:30 | Coffee break |
| 11:00 | Ulf: Benchmarking compile-time performance of Agda programs |
| 11:20 | Groups/Code sprints/Discussions |
| 12:00 | Lunch |
| 13:00 | Groups/Code sprints/Discussions |
| 15:30 | Coffee break |
| 16:30 | Groups/Code sprints/Discussions |
| 17:00 | Péter: Presentation of the new generalize/variable feature |
| 17:30 | Wrap-up meeting |
| Friday, 19 Oct | |
| 07:30 | Running excursion to Wollaton Park. Meeting location: Canal towpath by Wilford St |
| 10:00 | AIM XXIX location discussion with a special guest |
| 10:30 | Temporarily need to move to JC-DEARING-B19 |
| 12:00 | Lunch |
| 13:30 | Groups/Code sprints/Discussions |
| 15:00 | Coffee break |
| 15:30 | Andreas: Runnable interpreter for an intrinsically well-typed fragment of C in Agda |
| 16:30 | Groups/Code sprints/Discussions |
| 17:30 | Wrap-up meeting |
| Saturday, 20 Oct | |
| 09:30 | Talk slot: volunteers? |
| 10:30 | Coffee break |
| 11:00 | Groups/Code sprints/Discussions |
| 12:00 | Lunch (not Aspire) |
| ... | ... |
| ??:?? | Final discussion |
Talks/Presentations/Discussions
Presentations on theory, implementation, and use cases of Agda and type theory are welcome. If you would like to give a presentation, please write to Nicolai.
- Niels: Eliminating Traversals in Agda; brief abstract: We discuss a formalization of Bird's ‘replaceMin’ program (replaces all values in a tree by the minimum in one traversal) in Agda using Sized Types. Agda code on GitHub.
- András: Constructing Quotient Inductive-Inductive Types
- Nisse: Total Definitional Interpreters for Looping Programs
- Péter: Present the new generalize/variable feature
- Andreas: Lessons learnt from implementing a runnable well-typed interpreter for C– in Agda
Code sprint suggestions
- John / Ben: Edit-time tactics / Auto (related in Idris)
- Rethinking interleaving of functions and datatypes (Issue #2858).
- Matthew: Making in-file pragmas consistent across files, e.g. --safe, --without-K (Issue #2487). Maybe also: project-global options in the .agda-lib file
- Andreas: Runtime irrelevance via the 0 modality
- Péter, Ulf: Close issues labeled with 'generalize'.
- Guillaume: type providers
- Thorsten: Cubical+2-Level+Ind Families
Wrap up meetings
A short summary of the daily progress will be added.
- John / Ben: Edit-time tactics / Auto (related in Idris)
- Jesper: here's a small example tautology solver
[Monday] just started. [Tuesday] John gives a demo! 2+2 = 4. And then tautologies. You can write context dependent Agda edit tactics. [Thursday] Jesper gives a demo of mini-auto written in Agda. Hasn't yet tried the Riemann hypothesis. He has implemented a little tactic language in order to write mini-auto. [Friday] Some work on improvements. Docs are in the changelog and in the manual. The tactic library is now monadic and uses continuations. You can now write proof scripts as do blocks. [Saturday] Got merged into master. Refactoring not quite done, so that type checking is only once. [Saturday] ataca is A TACtic library for Agda: https://github.com/jespercockx/ataca
- Rethinking interleaving of functions and datatypes (Issue #2858).
[Monday] Jesper not yet there. [Tuesday] Nobody is working on this. Jesper was busy with the previous point. [Friday] We dropped this.
- Matthew: Making in-file pragmas consistent across files, e.g. --safe, --without-K (Issue #2487). Maybe also: project-global options in the .agda-lib file
[Monday] Too exciting. Focusses on something even more exciting: the next release of the standard library. [Tuesday] Overexcited. We are going to scrap this.
- Andreas: Runtime irrelevance via the 0 modality
[Monday] Andreas spend the day familiarising himself with what he has done at the last Agda meeting. Promises demo for tomorrow. Secret application happened too. [Tuesday] Andreas has a failing test case (which is good). Will show more tomorrow. [Thursday] Andreas gives a presentation. You can now declare data which is not needed at runtime. Example: well founded recursion. Does this work for Bove-Capretta? [Friday] Andreas forgot about the question. But it is still interesting. [Saturday] Forgot again. Homework.
- Péter, Ulf: Close issues labeled with 'generalize'.
[Monday] Looked at the issues and made a very nice plan. There is a generalise branch where errors have been replaced by other errors. There will be a talk on Thursday.
[Tuesday] Ulf : Starting to execute the plan. In the moment everything is broken. There is hope. Peter is working on his presentation.
[Thursday] Peter has just given his presentation. This is now in the master branch. Will still add some documentation.
[Friday] Only Ulf left. Peter escaped to Hungary. Generalizable variables now in the module telescope. [Saturday] Peter has pushed some documentation (in the user manual). Ulf: Generalizable variable in records not possible. Ulf will make nicer error message. To address this we have to solve the long standing issue of how to check records.
- Guillaume: type providers
[Monday] No progress yet. Has worked on old patches.
[Tuesday] Guillaume did something else. Auto now solves all the goals.
[Friday] Guillaume fixed some bugs. Some functions should be moved back to the safe part (e.g. decidable equality for strings).
Some discussion on safety emerged. Are different extensions compatible. We don't understand negative occurrent of type parameters in inductive-inductive definition.
[Saturday] Erase implies uip even without K. Instead of having trustme as a primitive, we want to have erase as a primitive and implement trustee on top.
- agda latex (Nisse)
[Friday] Nisse discussed the need for inline.
Now Nisse broke Agda-latex so that old papers won't translate anymore. This was already broken. There is already some advice how to do things in the user manual. Is it uptodate?
[Saturday] Some discussion about backend default translation. It would be nice if there was a default translation. Isn't there a package which translates unicode into latex.
- Thorsten and Andrea: Cubical+2-Level+Ind Families
[Monday] In the moment ind families don't work. We can translate families into parametrised types (which work) via left Kan extensions. But this seems too complicated. Another idea is too add trans constructors. will explore this further.
[Tuesday] Did Vectors as an example (implemented trans and derived the recursor). Does this also work for inductive equality? We will see. If yes, it would be an alternative solution to the J-beta problem.
[Friday] Andrea explained some details of the cubical agda implementation. Filippo joined the effort. We still haven't checked inductive equality. May also need a cofibrant universe.
[Saturday] HITs and master are merged. Currently working on Id, if this works Andrea will implement a general solution. Non fibrant universes still need to be addresse, hopefully at the next Asda meeting.
- Fredrik's secret project
[Tuesday] You can throw errors from the library. Now also warnings.
[Friday] Secret project is finished. Non secret project is the safety flag.
- Niels, Niccolò, Andras,
[Monday ?] Guarded recursion in Agda with sized types. Just started.
[Friday] Got started on a presheaf model. Are using sized types in an unorthodox way.
[Saturday] Niels is doing some refactoring.
- Closing discussion: what are the most important issues.
Jesper: Defining a sound core Agda. Agda spec project.
Gun : Improving documentation.
Anton : Installation still too difficult. Windows installer from Aaron (used in Iowa). Wiki should be streamlined, still different instructions on different places.
Thorsten: Homework for Andreas justify sized types. What about indexed records?
Suggest having destructors instead of fields to specify dependent records.
What about machine learning to generate Agda code? Is anybody thinking about this?
Excursion
On Wednesday, 17 Oct, we will go to the Peak District. Please bring shoes suitable for walking/hiking.
Location
The meeting (or most of it) will take place in room C1 of our school:
School of Computer Science University of Nottingham Jubilee Campus Wollaton Road Nottingham, NG8 1BB United Kingdom
Google Maps, coordinates: 52.953489, -1.187355.
Currency
The currency is the British Pound (GBP or £), nowadays very cheap. Debit/credit cards are accepted almost everywhere. In some situations, a small charge will be applied if you pay minor sums like £5 by card, and some small businesses (street food etc) may not accept cards. There is an ATM close to the School of Computer Science, but it probably chargers horrendous exchange fees. I (Nicolai) can give you £ for € if you want to exchange small amounts, or I can pay for you and you can pay me back in €.
Travel to Nottingham by Plane
Suggestions:
- East Midlands Airport (EMA): A small airport, and chances are that you won't find any suitable flights. If you do, you can take the Skylink bus to Nottingham city centre, or directly go by taxi to your hotel for ~30 GBP.
- Birmingham (BHX): From the airport, you can get to Nottingham in around 1:40 by train. Usually, a single change at Birmingham New Street is sufficient.
- Manchester (MAN): To Nottingham, it takes around 2:20 by train. Most connections only require a single change at Manchester Piccadilly.
- Stansted (STN) and other London airports: Not recommended, but still okay if there is nothing better and if you choose the right route. From STN, you can get to Nottingham in 3 hours with only one change in Ely or Leicester. Avoid connections through London, those will be more expensive, require more changes, and are generally more stressful!
From the train station: either go by taxi (~7 GBP) or walk to Victoria Centre, from where you can take the bus lines 28 and 30 to Jubilee Campus.
Accommodation
The P&J hotel is in good location and has previously been used for meetings in Nottingham. Unfortunately, campus accommodation is NOT available, sorry. booking.com and similar websites work well in Nottingham. Living in the city centre is an option. The School of Computer Science is on Jubilee Campus, reachable from the city centre in 40 minutes (walking time) or ~15 minutes (bus 28 or 30 + walking).
Lunch Menu (Aspire)
Monday
- Leek and potato soup
- Cumberland sausage swirl served with mashed potato, steamed vegetables & onion gravy
- Smoked haddock & macaroni cheese fishcakes served with salad, new potatoes and wholegrain mustard mayo
- Soya mince and vegetable chilli served with rice and sour cream (v)
Tuesday
- Mushroom and tarragon soup
- Chicken cacciatore served with penne and a rocket and parmesan salad
- Teriyaki salmon served on a bed of vegetable and noodle stir fry
- Potato, spinach and onion frittata served with salad and new potatoes (v)
Wednesday: we will eat in Edale (update: lunch Castleton, dinner Edale)
Thursday
- Sweet potato and cumin soup
- Chicken korma served with rice and mini poppadoms
- Roasted salmon fillet on a bed of spicy prawn and tomato fusilli
- Falafel and spinach burger served with sundried tomato mayo, lettuce, red onion and beef tomato (v)
Friday
- Tomato and red pepper soup
- Minced beef cannelloni served with garlic bread & salad
- Battered hake served with chips, peas, tartare sauce and a lemon wedge
- Roasted vegetable and goat’s cheese puff pastry tart served with salad, new potatoes and a roasted red pepper coulis (v)