Agda Implementors’ Meeting XXI

The twenty-first Agda Implementors’ Meeting will take place in Göteborg 2015–06–03 to 2015–06–09 (Wed to Tue). 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

2015–05–22
Registration deadline
2015–06–03 to 2015–06–09
AIM XXI

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.

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). (A receptionist should be sitting by the entrance, and will be able to help you find your way.)

Lunch and coffee breaks will be provided, as well as WIFI through eduroam.

Saturday 6th 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 7th: Walking on the Bohusleden, stage 3 from Kåsjön to Skatås. Bring:

  • outdoor shoes
  • water
  • lunch
  • rain gear / sun screen, depending on the weather
  • swimsuit & towel, if you are up to swimming in Härlanda tjärn
09:50 Meet at Korsvägen
10:07 Bus 513 to Kåsjön
10:27 Start hiking!
... hiking ... lunch ... swimming? ... coffee ...
18:00 We should be done.

Rough time estimate: Hiking (3 hours), breaks (2 hours), coffee (1 hour), trip back (1 hour). Café Skatåsmålet, Olbersgatan, 41655 Göteborg, tel: +46–31–250840, or Torps Café, Kyrkåsgatan 13, 41656 Göteborg, tel: +46–31–254360.

Dinner

Monday, 8 June, 7pm, at the http://www.flyingbarrel.se/, partially sponsored by https://www.fireeye.de/ Dresden.

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/Artemis.

Exceptions:

  • Thursday afternoon we meet in FL52 (Fysikhuset, Chalmers campus).
  • Saturday we meet in the Chalmers lunchroom (floor 8 of EDIT building).

Program

(not etched in stone)

Wed, June 03
09:30 Andreas Abel: 10 years of Agda2
10:25 Personal introductions and sprint suggestions
11:00 Coffee
11:30 Anton Setzer, Karim Kanso's PhD thesis integrating model checking and SAT into Agda
12:00 Anton Setzer, How to Reason Informally Coinductively
12:30 Lunch

Thu, June 04 [EARLY START!]
09:00 Jesper Cockx, Unification in a context of postponed equations
09:45 Ulf Norell, Reflections about reflection
10:30 Coffee
11:00 Nicolas Pouillard, Programming with linear types, a tutorial
12:00 Lunch
MOVE to FL52 for the afternoon.

Fri, June 05
09:30 Anders Mörtberg, An Implementation of a Cubical Type Theory
10:15 Bas Spitters, Cubical sets as a classifying topos
11:00 Coffee
11:30 Peter Dybjer, Implementing Martin-Löf's meaning explanations in Agda
12:30 Lunch

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

Sun, June 07
09:50 Excursion (Korsvägen!)

Mon, June 08
09:30 Thorsten Altenkirch, Type Theory eats itself --- without indigestion (joint work with Ambrus Kaposi)
10:15 Coffee
10:45 Christoph-Simon Senjak, An Implementation of Deflate in Coq
11:30 Keiko Nakata, Formal verification at FireEye
12:30 Lunch
19:00 Dinner at the Flying Barrel

Tue, June 09
09:30 Code sprints

AIMXXI Wrap up meetings

Travel to Göteborg

Local airports: Landvetter.

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.

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 a fee of 1000kr (~106 EUR) which you can pay here.

Participants

Andreas Abel, Gothenburg University (co-organizer) +49–179–40033323
Stephan Adelsberger, WU Wien
Guillaume Allais, Strathclyde U
Thorsten Altenkirch, Nottingham (invited speaker)
Guillaume Brunerie, Nice
Ana Bove, Chalmers
James Chapman, IoC Tallinn
Jesper Cockx, KU Leuven
Nils Anders Danielsson, Chalmers
Peter Dybjer, Chalmers
Hans Bugge Grathwohl, Aarhus U
Pepijn Kokke, Utrecht U
Yoshiki Kinoshita, Kanagawa U
Paul Laforgue, Lille University
Victor Lopez Juan, Chalmers
Guilhem Moulin, Chalmers
Keiko Nakata, FireEye Dresden (invited speaker)
Bengt Nordström, Chalmers (co-organizer)
Ulf Norell, Chalmers
Nicolas Pouillard, Copenhagen
Christoph-Simon Senjak, LMU München
Anton Setzer, Swansea U (invited speaker)
Bas Spitters, Aarhus U
Makoto Takeyama, Kanagawa U
Andrea Vezzosi, Chalmers (co-organizer) +46–72–6504642
Matthew Wilson, Formal Solutions
Theo Winterhalter, ENS Cachan

Talks

Andreas Abel, 10 Years of Agda2
Anton Setzer, How to Reason Informally Coinductively. PhD Thesis, source code and MRes thesis by Karim Kanso
Jesper Cockx, Unification in a context of postponed equations (Slides).
Nicolas Pouillard, Programming with Linear Types, a tutorial (Slides, Tutorial).
Anders Mörtberg, An Implementation of a Cubical Type Theory (Slides).
Peter Dybjer, Implementing Martin-Löf’s Meaning Explanations in Agda (Agda-files).
Christoph-Simon Senjak, An Implementation of Deflate in Coq.
Ulf Norell, Reflections on Reflection.

Jesper Cockx, Unification in a context of postponed equations

Agda’s algorithm for checking definitions by dependent pattern matching relies a great deal on unification. On the one hand, we want this unification algorithm to be as powerful as possible, in order to accept more definitions. On the other hand, there is a desire to be conservative with respect to the standard axioms of type theory. One area of tension between these two desires is the postponing of equations. The theory doesn’t say anything about it, yet the implementation happily postpones any equation they can’t solve right away. That this leads to problems, can be seen in issues both old (Issue 292) and new (Issue 1406, 1435). In an attempt to fix these problems, forcing rules were added, allowing Agda to skip unification of certain arguments when they must be equal because of the type. However, the current implementation doesn’t have enough information available to make a correct decision when to apply forcing, leading to other problems (Issue 1427).

Rather than restrict the current postponing mechanism to avoid these problems, I propose to rebuild unification up from the foundations with postponed equations in mind. The central idea to do this is to keep track of how the type of each equation depends on which previously postponed equations. This is done by introducing a new variable for each postponed equation, serving as a placeholder for the solution of that equation until it is solved. It turns out that having this context of postponed equation actually allows us to apply more unification rules, giving us a solution where previously there was none. To take advantage of this benefit, I introduce the idea of reverse unification rules, which can introduce new postponed equations or combine them when this is useful. It turns out that these reverse unification rules subsume the rules for skipping unification of forced constructor arguments.

In my presentation, I will delve into some examples where postponed equations are useful, and also some examples of what goes wrong when it is implemented naively. After that, I will discuss my proposal how to handle postponed equations in general: first, the beautiful theory of working in a context of postponed equations, then the complex art of applying reverse unification rules to bring these postponed equations in just the right form, and finally the ugly practice of implementing all of this.

Thorsten Altenkirch, Type Theory eats itself --- without indigestion (joint work with Frederik Forsberg and Ambrus Kaposi)

Implementing a total syntax for a language with dependent type incurred a huge overhead due to having to be explicit about families of setoids etc. We propose to use first order Higher Inductive Types with we call QITs (Quotient Inductive Types). They already play an important role when formalizing infinitary algebraic theory like the Cauchy Reals in the HoTT book. A simple example is given by infinitely branching trees quotiented by permutation. The definition using quotient is unsatisfactory because we cannot lift the node constructor without using countable choice. A similar problem has recently been observed in the context of the partiality monad by Uustalu et al.

As far as TT in TT is concerned we have formalized a basic type theory with recursor and eliminator and have implemented the set-theoretic semantics using the recursor. The formalisation of the logical predicate translation and the presheaf interpretation is work in progress. The latter would lead to NBE which requires a definition of normal forms. However, it turns out that the definition of normal forms already requires normalisation. Also we observe that you need truncation or UIP to define normal forms.

See https://bitbucket.org/akaposi/tt-in-tt