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

Registration and talk proposal deadline. Registration form

Talk proposals: You can propose a talk when you register, or afterwards using talk proposal form

2017–05–09 (Tu) to 2017–05–15 (Mo)

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.


You register for the meeting by filling out this registration form

There is no registration fee. Transportation, accommodation and meals are to be covered by the participant.

Please register as soon as possible to help us with planning.


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
  • comfortable shoes
  • water
  • lunch
  • rain gear / sun screen, depending on the weather
  • swimsuit & towel, if you are up for swimming.
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
13:30 Continue hiking
14:00 Break (~½ hour)
16:00 Reach Bohus fortress
... Tour around Kungälv
      - Walk around Bohus fortress
      - Check out the old city center
      - Have coffee
18:00 Take Grön Express back to Gothenburg

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 from 11am to 4pm. There is a small nature reserve nearby, Fontin.


Those who want to can join for dinner Thursday, 11th May, 7pm, at NOBA Nordic Bar. location, menu (250 - 380 SEK pp).

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.


  • Friday and Monday we meet in Chalmers Konferenscenter (in front of the Chalmers tramstop).
  • Saturday we meet in the Chalmers lunchroom (floor 8 of EDIT building).


(not etched)

Tu, May  9
10:15 Coffee
10:30 Personal introductions and sprint suggestions
12:30 Lunch

Wed, May 10
10:15 Coffee
12:30 Lunch

Thu, May 11
10:15 Coffee
12:30 Lunch
19:00 Dinner

Fri, May 12
10:15 Coffee
12:30 Lunch

Sat, May 13
10:00 Meet at EDIT main entrance.
The door will be closed, so call +46705754236 (Victor) to let you in if you arrive later 
Then: Hacking in Chalmers EDIT lunchroom

Sun, May 14
09:50-18:00 Excursion

Mon, May 15
10:15 Coffee
12:30 Lunch      

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.

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.


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.


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:


  • Jesper Cockx, KU Leuven
  • Víctor López Juan, Chalmers
  • 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


Andreas Abel: Eat your own dog food

Remarks on the Agda development process.

Ulf Norell: TBD

Peter Dybjer: Higher Inductive Types in the Groupoid Model

Wolfram Kahl: TBD

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

The future of annotations on function spaces in Agda.

Jonathan Prieto-Cubides: Proof Reconstruction in Classical Propositional Logic

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.