Agda Implementors' Meeting XXIX

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.

Important dates

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)



If you are a citizen of countries listed here, you can visit Japan without applying for a visa. Otherwise, please contact Youyou.

Power adaptor

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


    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:00Meet up at Myogadani station
10:30Introduction, etc.
10:40Andreas: How to represent it in Agda
11:10Code Sprints Suggestions
13:00Code Sprints
16:30Wrap-up Meeting
Thursday, 14 Mar
09:00Lambda Piano Concert, Students Commons, 2F
10:30Chiaki: Proof search for equational reasoning
13:00Jesper's tutorial
14:00Code Sprints
16:30Wrap-up Meeting
Friday, 15 Mar
10:30Yutaka: Machine Learning for Isabelle/HOL and Agda (paper)
11:30Excursion (Koishikawa Botanical Garden)
Saturday, 16 Mar
10:30Jesper: How to tame your rewrite rules
11:00John: Type Theory as API
13:00Code Sprints
16:30Wrap-up Meeting
Sunday, 17 Mar
 Excursion (10:30 at Takaosanguchi station)
Monday, 18 Mar
10:30Ulf: Algebraic Effects in Agda
11:00Code Sprints
13:00Code Sprints
16:30Wrap-up Meeting
Tuesday, 19 Mar
10:30Shinji: On our Agda experience in Category theory, Hoare logic, Automaton and System F
11:00Code Sprints
13:00Code Sprints
16:30Wrap-up Meeting

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

Wrap-up meeting

  • 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

  • Thursday
    • 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.

Page last modified on March 19, 2019, at 07:50 am
Powered by PmWiki