The eighteenth Agda Implementors' Meeting will take place in Göteborg 2013-09-12 to 2013-09-18 (Thu to Wed). Everyone who uses Agda is invited to attend. The meeting will be similar to previous ones:
- Presentations and discussions.
- Plenty of time to work on or in Agda, in collaboration with the other participants.
Important dates
- 2013-08-30
- Deadline (soft) for registration
- 2013-09-12 to 2013-09-18
- AIM XVIII
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.)
For late evening and weekend hacking the lunch room of the department can be used.
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.
If you have trouble finding your way you can call one of the organisers: Dan Rosén (+46-72 96 36 126) or Guilhem Moulin (+46-31 772 54 10).
Projects
Sprints (topics to work on):
- Type-theory in Color (Guilhem Moulin, Jean-Philippe Bernardy)
- add as a feature in Agda
- Thursday: new bugs were discovered, computational content is yet to be added (fixed)
- Monday: issue: Unclear what should be the status of erased definitions.
- Tuesday: possible fix: add the colors that are to be erased in the definitions itself (TypeChecking.Monad.Base.Defn`).
- Wednesday: still in the middle of the development
- Windows installer (Makoto Takeyama)
- Thursday: experiment: which component is needed for the installer to work? TODO: Agda no longer uses the Haskell-mode
- Monday: New links have been added to the windows installer page. Should the Haskell platform be part of the Windows installer (required for compilation)? Not clear which fonts should come with the package. Bundling is tricky to do with GPL-flavored licenses. Makoto's idea: Build the installer as part of the release. Nisse's answer:
none of the people who currently release Agda are running Windows. Possible fix: Find a replacement on the Agda mailing-list.
- package without the need for separately installing the Haskell Platform.
- Bengt's suggestion: we could get some ideas from other projects (the Grammatical Framework for instance). Ideally, a Cabal-like could be written for Agda.
- structured semi-formal arguments (Makoto Takeyama, Bengt Nordström, Yoshiki Kinoshita)
- working on a "request for proposal" (to take existing languages closer to Agda?)
- Thursday: some discussion took place, nothing concrete has been decided
- Co-patterns and co-induction (Andreas Abel, Bengt Nordström)
- Some missing pieces in frontend (almost done)
- how to compile?
- Thursday: State of the art: no longer preprocessed but part of the core on Andreas' local worktree (activated with the `--copatterns` flag). Check for productivity. Some more bugfixes are required before merging, and some preservation properties need to be specified.
- Worked on the integration with the `with` construct, which turned out to be harder than expected.
- Pushed \o/. Doesn't work with `with` yet; there's also a syntax issue with instance arguments. And the feature has an efficiency issue since non co-inductive terms are uselessly reduced when comparing.
- Finish new version of Agsy and connect it to Agda (Fredrik Lindblad, Andreas Abel, Ulf Norell)
- + integrate test suite
- present ord discuss Agsy interface
- Prototyping for efficiency tests (Ulf Norell, Nils Anders Danielsson, Andreas Abel, Fredrik Lindblad)
- identify performance problems and possible solutions
- representations of substitutions, names etc.
- ideas from lambda-prolog
- compare with Agsy representations (delayed substitution, etc.)
- examples from Fredriks TPTP lib. translated to Agda
- Thursday: Designed a syntax (subset of Agda including records, datatypes, I-R, equality, Π, meta-variables), implemented a parser. A type system is yet to be fleshed out.
- Friday: implemented parser and scope checker, type system fleshed out
- Monday: worked on a simple implementation, perhaps not so efficient, but that should get the typing rules right. Next step: Improve efficiency.
- Tuesday, Wednesday: Continue to work on the baseline, inefficient implementation.
- Parallel Parsing formalization (Jean-Philippe Bernardy, Patrik Jansson)
- ICFP paper formalization, uses "almost near semirings", matrix multiplication and Valiant's algorithm
- Tuesday: Done! \o/. (Two minor issues.)
- Wednesday: no more hole.
- Sequential decision problems formalization (Patrik Jansson, Nicola Botta)
- explore and port parts of an Idris development to Agda
- translated a few modules. We're waiting for a demo.
- Core language (JPB, Guilhem Moulin, Andreas Abel, Bengt Nordström, Fredrik Lindblad)
- discussion and implementation
- presentation by JPB Friday morning at 9.15 in EDIT 3364
- discussed suject-reduction issues with Nisse.
- Gabriel is now up-to-date. More discussion on the design.
- Setoids (Yoshiki Kinoshita)
- Background: started from proving the Yoneda lemma, didn't work for propositional equality => refactored into Setoid based development
- change implementation of NBE proof to use equivalence relations
- Thursday: postulated the Univalence Axiom, got some ideas how
- Implicit Coercions discussion inspired by Coq (Guillaume Brunerie, Bengt Nordström, Ulf Norell)
- Thursday: Coercions can be implemented using instance arguments. It doesn't compose though, and InstanceSearch is quite slow, and limited to name lookups. Makoto's hint: Another solution is to use a hidden index, at least when the the index is inferable. Nisse: If one doesn't want to add explicit coercions then Agda needs to be changed; otherwise there are already ad-hoc solutions. Guillaume: Perhaps the search algorithm could be changed to be faster.
- Web service for coding Agda in your browser (Dan Rosén, Bengt Nordström)
- Peter Diviansk has done some earlier work
- Tuesday: Mailed Peter. Idea: Compile Agda to JavaScript; many compilation errors. The JS code would probably be too big anyway. An alternative would be to have Agda on the server and use it as a JS library (with a JS editor which would mimic the agda-mode).
- Wednesday: Got some answer from Peter, he'll make his work available somewhere. Idea: Import Agda as a library, and make the browser communicate with the backend through a websocket using JSON-formatted expressions.
- Simplification (Guillaume Brunerie, Andreas Abel)
Tuesday: Idea (bug #850): Only reduce ι-redexes (cf. `simpl` in Coq). Makoto: Would be good to be able to specify which commands are to be unfolded.
Schedule
(not set in stone)
Thu Sept 12
09:00 Introduction and planning
10:00 Fika
10:30 Talks:
Yoshiki Kinoshita: Agda proof of NBE for categories.
Andreas Abel: Agda as a Library?! Modularization of the Implementation and Stuff
12:30 Lunch
13:30 Hacking
15:00 Fika, then hacking
16:30 Wrapping up (progress reports)
19:00 Dinner
Fri Sept 13
09:00 Gathering, (EDIT room 3364) <- Note the room!
09:15 Talk (EDIT room 3364)
Jean-Philippe Bernardy: Presentation and discussion about Core Language
10:00 Talk (EDIT room 3364)
Nicola Botta: Sequential decision problems, dependently typed solutions
Abstract:
We present a dependently typed formalization for a simple class of sequential
decision problems. For this class of problems, we derive a generic
implementation of Bellman's backwards induction and a machine checkable proof
that the implementation is correct. We discuss the problem of extending the
formalization to time-dependent monadic decision problems.
11:00 Fika, then hacking
12:30 Lunch
13:30 Hacking
15:15 Fika, then hacking
16:30 Wrapping up
19:00 Dinner, at LinnéTerrassen
Sat Sept 14
Excursion, to Marstrand
Evening event: Concert with The Western Toneflyers at the new KoM restaurant
Sun Sept 15
Optional coding day in the EDIT lunch room on the 7th floor
Mon Sept 16
09:00 Talk: Guillaume Brunerie: What is missing for Agda to be suitable for Univalent Foundations?
10:00 Fika, then hacking
12:30 Lunch
13:30 Hacking
15:15 Fika, then hacking
16:30 Wrapping up
19:00 Dinner
Tue Sept 17
09:00 Hacking
10:00 Fika, then hacking
12:30 Lunch
13:30 Hacking
15:15 Fika, then hacking
16:30 Wrapping up
19:00 Dinner
Wed Sept 17
09:00 Hacking
10:00 Fika, then hacking
12:30 Lunch
13:30 Final wrap up
14:30 Talk: Thierry Coquand: Univalent thoughts
15:15 Fika
16:00 Discussion about AIM XIX. James Chapman has suggested Tallinn. Should AIM XX be held in connection with ICFP in Gothenburg? (The main ICFP 2014 conference will take place 2013-09-01/03 with workshops the (sun)day before and the three days after.)
19:00 Dinner
Travel to Göteborg
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.
Local airports: Landvetter and Göteborg City Airport.
Accommodation
You may want to use SGS Veckobostäder (330 SEK/night for a single room if you stay for 8 nights). There are many other options.
Social events
No coding on Saturday 14
Excursion
We will spend the day in Marstrands. Departure from Hjalmar Brantingsplatsen at 10:29. Hjalmar Brantingsplatsen is a central hub for busses & trams; from Chalmers the simplest is to take the 6th tram (25min ride, direction Länsmansgården) or the 10th (15min ride, direction Biskopsgården). Buss and tram tickets cannot be bought onboard, you need to go to a Västtrafik or Pressbyrån kiosk; tell them you want to go to Marstrand to get the proper fare.
- Bus Grön Express to Ytterby (direction Kungälv/Ytterby) -- 10:29-11:02
- Marstrand Express to Marstrand's ferry terminal -- 11:07-11:36
- Ferry 322 to Marstrandsön -- 11:52-11:54
(Back same route, departure at 16:15; public transports go on every two hours only.)
What to see:
Concert
On saturday evening we'll try to find a table (wasn't possible to book) to KoM Musik & Bar to have dinner and listen to The Western Toneflyers. The stage in on Karl Johansgatan 15; the closest stop is Kaptensgatan, and trams 3 and 9 lead there from the central station.
Dinner
The official dinner will take place in LinnéTerrassen on Friday 13 around 19h. We will walk there from the university, but if you want to go on your own, you will find LinnéTerrassen on Linnégatan 32. The closest tram/bus stop is Linnéplatsen, and many trams lead there.
Registration
You register for the meeting by filling out the form below and emailing it to Guilhem Moulin.
Attendance is free, and includes lunch and fika twice a day. Otherwise, participants need to cover all expenses themselves.
The Agda meeting is sponsored by the EU FP7 project GSDP and is part of the effort to define the computer science part of Global Systems Science. If you do research in connection with global systems science then you can apply for funding to cover travel or accommodation expenses. Please email Guilhem as soon as possible if you want to do so.
If you want to give a talk, or lead a discussion on some subject, indicate so on the registration form. We will let you know whether your proposal is accepted closer to the meeting. (The "code sprints" form the core of the meeting, so we do not want to spend too much time on talks and discussions.)
Registration form Agda Implementors' Meeting XVIII Name: Title and abstract (if you want to give a talk or lead a discussion): Additional comments:
Participants
- Andreas Abel, Gothenburg University
- Stephan Adelsberger, Vienna University
- Jean-Philippe Bernardy, Chalmers
- Ana Bove, Chalmers
- Guillaume Brunerie, University of Nice
- Nils Anders Danielsson, Gothenburg University
- Peter Dybjer, Chalmers
- Patrik Jansson, Chalmers
- Yoshiki Kinoshita, Kanagawa University (has to leave on Sunday)
- Guilhem Moulin, Chalmers
- Ulf Norell, Gothenburg University
- Gabriel Radanne (Monday-Wednesday only)
- Bengt Nordström, Chalmers
- Dan Rosén, Chalmers
- Christoph-Simon Senjak, LMU
- Makoto Takeyama, Kanagawa University
Talks
- Yoshiki Kinoshita: Agda proof of NBE for categories.
I wish to explain my Agda code of NBE for categories. An obvious generalisation of the classical topic---NBE for monoids. The aim of the talk is not to insist on the generalisation, but to present my formalisation of E-categories, some syntax for that, and the need for discriminate inductive equality and the equivalence relation attached to homsets.
- Andreas Abel: Agda as a Library?! Modularization of the Implementation and Stuff
- Guillaume Brunerie: What is missing for Agda to be suitable for Univalent Foundations?
- Jean-Philippe Bernardy: Presentation and discussion about Core Language
- Nicola Botta: Sequential decision problems, dependently typed solutions (FP talk)
We present a dependently typed formalization for a simple class of sequential decision problems. For this class of problems, we derive a generic implementation of Bellman’s backwards induction and a machine checkable proof that the implementation is correct. We discuss the problem of extending the formalization to time-dependent monadic decision problems.
- Thierry Coquand: Univalent thoughts
Suggested time for AIM XIX
May 22-28 in Tallinn, Estonia.