The twenty-ninth Agda Implementors' Meeting will be held in Tokyo, Japan at Ochanomizu University from 13 March 2019 to 19 March 2019 (Wednesday to Tuesday). 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.
- Registration deadline
The deadline is soft, and if you miss it, you will still be very welcome to come. However, we would appreciate it if you could drop a line to Youyou.
- 2019-3-13 (Wed) to 2019-3-19 (Tue)
- AIM XXIX
If you are traveling from Europe, you might need a power adaptor. Please visit this website for more information.
Please register for this meeting by filling out the form below and sending it to Youyou.
There is no registration fee. Coffee breaks may be included. Transportation, accommodation and meals are to be covered by the participant. There will be an excursion which may cause additional costs for the participants as well. The details of excursion are to be decided, but if you have any preferences/suggestions (e.g., interested in old towns), please indicate in the registration form.
Registration form Agda Implementors' Meeting XXIX Name: Title and abstract (if you want to give a talk or lead a discussion; optional): Suggestions for code sprints (optional): Other remarks (optional):
- Youyou Cong
- Kenichi Asai
- Haruka Matsumoto
- Urara Yamada
- Naho Wakikawa
- Chiaki Ishio
- Tsukino Furukawa
- Mai Kitagawa
- John Leo
- Jesper Cockx
- Andreas Abel
- Zack Grannan
- Shinji Kono
- Yutaka Nagashima
- Ulf Norell
- Kenichi Kuga
- Mitsuharu Yamamoto
- ... your name could be here :)
Detailed program (suggestion, flexible)
|Wednesday, 13 Mar|
|10:00||Meet up at Myogadani station|
|10:40||Andreas: How to represent it in Agda|
|11:10||Code Sprints Suggestions|
|Thursday, 14 Mar|
|09:00||Lambda Piano Concert, Students Commons, 2F|
|10:30||Chiaki: Proof search for equational reasoning|
|Friday, 15 Mar|
|10:30||Yutaka: Machine Learning for Isabelle/HOL and Agda (paper)|
|11:30||Excursion (Koishikawa Botanical Garden)|
|Saturday, 16 Mar|
|10:30||Jesper: How to tame your rewrite rules|
|11:00||John: Type Theory as API|
|Sunday, 17 Mar|
|Excursion (10:30 at Takaosanguchi station)|
|Monday, 18 Mar|
|10:30||Ulf: Algebraic Effects in Agda|
|Tuesday, 19 Mar|
|10:30||Shinji: On our Agda experience in Category theory, Hoare logic, Automaton and System F|
Code Sprints Suggestions
- Shinji: direct handling of variables.
On the problem of induction on data types using Church encodings see also Aaron Stump, Dependent Lambda Encodings.
- Andreas: modalities
- John: specification
- Ulf: reflection
- Jesper: emacs command for missing clauses, Literate Agda, double-check option
- Zack: extend standard library with concepts from rewriting theory
- Youyou: Agda for math education
- Day 1
- Andreas, Shinji: discussed how to use Agda as predicative System F; induction on Church encodings needs an extension, see Cedille's dependent intersection
- Chiaki, Kenichi, Ulf: discussed how to generate error messages and tactics using the reflection library
- Ulf: trying to steal the effects library from Idris
- Jesper: improving debugger output
- Zack: adding rewriting concepts to the standard library
- John, Youyou: trying to extend John's music tools
- Day 2
- Andreas: HOAS on top of de Bruijn
- Ulf: supported file IO
- Jesper: fixed a problem with Prop
- Zack: formalizing normalization-related properties
- Shinji: getting ready for trying Jesper's tactics
- John, Youyou: formalized motions and first species counterpoints
- Chiaki, Kenichi: tactics for automatically reducing STLC terms
- Day 4
- Andreas: debugging Issue #3211
- Ulf: discovered segfalt
- Jesper: making rewriting rules work modulo eta equality
- Zack: formalization of normalization theorems
- Shinji: found an issue with Yoneda
- Chiaki: tactics for multi-step reduction
- John, Youyou: reduced the number of constructors
- Day 6
- Andreas: fixed performance regression in 2.5.4
- Ulf: more on segfault, effect examples
- Jesper: analyzing metavariables that block reduction
- Zack: formalizing Newman's lemma
- Shinji: trying to understand reflection
- Chiaki, Kenichi: tactics for single-step reduction (harder than multi-step!)
- John, Youyou: created counterpoint for Yamanote melody
- Day 7
- Ulf: documentation for automatic generalization of variables
- Jesper: released notes for new Agda; pull request on dependent pattern matching
- Zack: finished Newman's lemma; looking at coinductive datatypes for binary relations
- Kenichi: formalizing one-pass CPS (with de Bruijn indices)
- Youyou: writing a talk on simulating algebraic effects with multi-prompt shift/reset
Lambda Concert Program
- Youyou: Sonata in B minor & Ballade No. 1 (Chopin)
- Kenichi: Polonaise in C minor & Nocturne in E major (Chopin)
- Chiaki: Tempest Sonata (Beethoven)
- John: German Dance (Haydn)
The meeting will take place in Room 602 of Faculty of Science, Building 3 (marked 20 in this map).
Ochanomizu University 2-1-1 Otsuka, Bunkyo-ku, Tokyo 112-8610, Japan
We could meet up at the Myogadani Station on the first day and walk to the campus together.
Travel to Tokyo by Plane
Tokyo is served by two airports: Haneda (HND) Narita (NRT). Haneda airport is closer to the city center, but direct flights from U.S./European countries are limited.
There are a lot of hotel options in the Korakuen and Ikebukuro area, which are one/two stops away from the campus. Here are some recommendations:
Lunch is not included, but the university has a cafeteria, where you can find reasonably priced (and not so bad) food. There are also several restaurants and convenience stores around the campus. Note that Japan is not vegetarian-friendly. If you have any dietary restrictions, Youyou will help you find things that meet your needs.