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

2019-3-1

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

Caveats

Visa

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.

Registration

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):

Participants

• 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)

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)

Location

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.

Accommodation

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:

• https://www.booking.com/hotel/jp/koraku-garden-hotel.en-gb.html
• https://www.booking.com/hotel/jp/richmond-tokyo-suidobashi.en-gb.html
• https://www.booking.com/hotel/jp/centurion-ikebukuro.en-gb.html
• https://www.booking.com/hotel/jp/flexstay-higashi-ikebukuro-inn.en-gb.html

Lunch

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.