Agda Implementors' Meeting XXV

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:50Meet at Central Station
10:10Take tram #4, buss 76 to Rannebergen
10:45Hike!
12:30Lunch, swimming? in Gäddevatten lake
13:30Continue hiking
14:30Break (~½ hour)
16:00Reach Bohus fortress, tour around Kungälv
18:00Take 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.30Session 1: Talks & Discussions
10.30Coffee break
11.00Session 2: Talks & Discussions
12.00Lunch
13.15Code sprints
15.00Coffee break
15.30Code sprints
17.30Wrap-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.30Andreas Abel: Eating your own dog food
10.15Introduction, code sprint proposals, planning
10.45Coffee break
11.15Jesper Cockx: Modalities and polarities
12.00Lunch
13.15Code sprints
15.00Coffee break
15.30Code sprints
17.30Wrap-up meeting
Wednesday, May 10
09.30Niels van der Weide: Higher Inductive Types in Programming
10.30Coffee break
11.00Andrea Vezzosi: Cubical Type Theory in Agda (demo code)
12.00Lunch
13.15Code sprints
15.00Coffee break
15.30Code sprints
17.30Wrap-up meeting
Thursday, May 11
09.30Jonathan Prieto-Cubides: Proof Reconstruction in Classical Propositional Logic
10.30Coffee break
11.00Thierry Coquand: Partial type theory
12.00Lunch
13.15Code sprints
15.00Coffee break
15.30Code sprints
17.30Wrap-up meeting
19.00Dinner @ Noba
Friday, May 12
09.30Guillaume Allais: agdarsec - Total Parser Combinators
10.30Coffee break
11:00Peter Dybjer: Higher Inductive Types in the Grupoid Model
12.00Lunch
13.20Anton Setzer: Programming GUIs with Agda
14.20Code sprints
15.00Coffee break
15.30Code sprints
17.30Wrap-up meeting
Saturday, May 13
09.30Wolfram Kahl: (Re-)Creating Sharing in/for the GHC back-end of Agda
10:30Coffee break
11.00Fredrik Nordvall Forsberg: Variations on inductive-recursive definitions
12.00Lunch
13.30Code-sprints
15.00Coffee break
15.30Víctor López Juan: How to write documentation (tutorial)
16.00Jonathan Prieto-Cubides: A purpose of a package manager for Agda (demo)
16.30Code-sprints
17.30Wrap-up meeting
Sunday, May 14
10.00Excursion
19.00Back in Gothenburg
Monday, May 15
09:30Ulf Norell: Mystery Talk
10:30Coffee break
11:00Code sprints
12.00Lunch
13.15Code sprints
15.00Coffee break
17.30Wrap-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:

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

demo code

Jonathan Prieto-Cubides: A package manager for Agda (demo)

Github repo

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.