The thirty-second Agda Implementors' Meeting will take place between 2020-05-25 and 2020-06-05. Everyone who uses Agda is invited to attend.

Due to the current pandemic the meeting will be held online. It will be held over two weeks instead of one, but each day might be less intense than in previous meetings. We will try to accommodate participants from different time zones. Please indicate at what times of the day that you are available when registering.

(An aside related to numbering: AIM XXXI was postponed. It is planned to be held later, and has kept its number. Thus AIM XXXII might be held before AIM XXXI.)

## Important dates

- 2020-05-10
- Soft deadline for registration
- 2020-05-11 to 2020-05-15
- People can express interest in code sprints
- 2020-05-25 to 2020-06-05 (weekdays only)
- AIM XXXII

## Registration

You register for the meeting by entering your name below. Registration is not compulsory. Please also enter proposals for talks, discussions and code sprints below.

## Technology

It is likely that talks and discussions will be held via Zoom. Code sprints will be coordinated on the Agda meeting Slack, which can be joined here.

## Programme

The following programme is preliminary. Links to Zoom (or something like that) will be added later. **Note: UTC is used for dates and times.**

- Monday 2020-05-25:
First session (Zoom):
- 10-11: Introduction
- 11-12: Discussion: Matthew Daggitt: Implementing refactoring tools for Agda

- 15-16: Thorsten Altenkirch: The symmetry of cubism
- 16-16:30: Wrap-up meeting

- Tuesday 2020-05-26:
- 13-14: Discussion: Jesper Cockx: Revising Agda's module system

- Wednesday 2020-05-27:
- 10-11: Discussion: Thorsten Altenkirch: Fixing cubical
- 11-11:30: Wrap-up meeting
- 15-16: Talk: Jesper Cockx: To infinity, and beyond! On the need for sorts bigger than Setω

- Thursday 2020-05-28:
- 12-13: Talk: John Leo: Music Tools

- Friday 2020-05-29:
- 10-11: Talk: Artem Shinkarov
- 15-16: Talk: Arjen Rouvoet
- 16-16:30: Wrap-up meeting

- Monday 2020-06-01:
- 12-13: Talk: Nils Anders Danielsson: Some tricks for making Agda code faster
- 13-13:30: Wrap-up meeting

- Tuesday 2020-06-02:
- 15-16: Talk: Uma Zalakain: π with leftovers: a mechanisation in Agda

- Wednesday 2020-06-03:
- 12-13: Talk: Joris Ceulemans: Modal Type Theory in Agda Using Presheaves
- 13-13:30: Wrap-up meeting

- Thursday 2020-06-04:
- 10-11: Talk: James Wood: Why does Dec look funny these days?

- Friday 2020-06-05:
- 12-14: Final wrap-up meeting

## Registered participants

If you are not working during "normal business hours" you may want to give a time zone that differs from the one in effect at your physical location.

Name | Time zone |
---|---|

Nils Anders Danielsson | UTC+2 |

Jesper Cockx | UTC+2 |

John Leo | UTC-7 |

Herminie Pagel | UTC+2 |

Jakob von Raumer | UTC+2 |

Jacques Carette | UTC-4 |

Fredrik Nordvall Forsberg | UTC+1 |

Víctor López Juan | UTC+2 |

Andreas Abel | UTC+2 |

Tesla Ice Zhang | UTC+8 |

Jannis Limperg | UTC+2 |

Matthew Daggitt | UTC+8 (probably available at ~ UTC+2) |

Yotam Dvir | UTC+2 |

Ulf Norell | UTC+2 |

Joris Ceulemans | UTC+2 |

Martin Escardo | UTC+1 |

Brent Yorgey | UTC-5 |

Liang-Ting Chen | UTC+8 |

Roman Kireev | UTC-2 |

Ting-Gan LUA | UTC+8 |

Orestis Melkonian | UTC+1 |

Evgeny Poberezkin | UTC+1 |

James Wood | UTC+1 |

Tomas Möre | UTC+2 |

Sandro Stucki | UTC+2 |

Jason Hu | UTC-4 |

Andrea Vezzosi | UTC+2 |

Zeji Li | UTC+1 |

Patrik Jansson | UTC+2 |

Chao-Hong Chen | UTC-4 |

Ana Bove | UTC+2 |

Thierry Coquand | UTC+2 |

Thorsten Altenkirch | UTC+1 |

Stefania Damato | UTC+2 |

Peter Dybjer | UTC+2 |

Anton Setzer | UTC+1 |

Reed Mullanix | UTC-8 |

Uma Zalakain | UTC+1 |

Adam Wyner | UTC+1 |

Stephan Adelsberger | UTC+2 |

Arved Friedemann | UTC+2 |

Nicolai Kraus | UTC+1 |

András Kovács | UTC+2 |

Ambrus Kaposi | UTC+2 |

Wen Kokke | UTC+1 |

Artem Shinkarov | UTC+1 |

Favonia | UTC-5 |

Wolfram Kahl | UTC-4 |

Scott Walck | UTC-4 |

Marko Dimjašević | UTC+2 |

Mietek Bak | UTC+2 |

## Talk proposals

List talk proposals here.

**Jesper Cockx: To infinity, and beyond! On the need for sorts bigger than Setω**Something about https://github.com/agda/agda/pull/4609**John Leo: Music Tools**An update on the progress of tools written in Agda for the analysis and synthesis of music. Joint work with Youyou Cong.**Joris Ceulemans: Modal Type Theory in Agda Using Presheaves**Presentation of work in progress on a shallow embedding of modal (dependent) type theories in Agda using presheaves.**Arjen Rouvoet: TBC****Artem Shinkarov: Extraction in Agda**I would like to share my experience of creating an extractor for a shallowly-embedded DSL. The extractor is written in Agda using the Reflection library. The interesting points are: turning a patten-mathcing lambda into a function with a nested conditional; translating type invariants into assertions of the target language; using rewrite rules to "optimise" expresions prior the extraction. For the latter the tricky bit was to push normalisation under the branches of the pattern-matching lambda, which requires to compute the valid typing context for the chosen branch of the pattern-matching tree.**Uma Zalakain: π with leftovers: a mechanisation in Agda**We use leftover typing on a set of partial commutative monoids to mechanise a π-calculus with shared, graded and linear channels.**James Wood: Why does**It used to be that the answer to a decision problem was either`Dec`

look funny these days?`yes`

followed by a proof or`no`

followed by a refutation. But now, using a recent version of the Standard Library, when you pattern match on a variable of type`Dec P`

, you get`does`

_{1}`because proof`

_{1}, leaving you little the wiser on what the result actually was. In this talk, I'll explain why this is a good (and sometimes crucial) thing, and what new best practices it entails for working with decision procedures.**Thorsten Altenkirch: The symmetry of cubism**In old agda we could do inductive proofs by pattern matching and structural recursion. My observation is that in cubical agda we can do coinductive proofs by copattern matching and guarded recursion. My message is that cubical is good for more then proving univalence or performing higher dimensional homotopical proofs inaccessible to ordinary mortals.**Nils Anders Danielsson: Some tricks for making Agda code faster**I plan to show some tricks I have used to make my Agda code type-check faster.**Name: Title**Abstract

## Discussion proposals

List discussion proposals here.

**Jesper Cockx: Revising Agda's module system**In the 13 years since the original release of Agda 2, the module system designed by Ulf Norell has proven itself to be powerful and robust for many applications. However, two pain points in the current implementation are the printing of names coming from imported modules, and the efficiency issues (e.g. https://github.com/agda/agda/issues/4331) arising from the need to copy modules on application. This would be a good time to revisit the original design and see what can be improved with our current knowledge.**Matthew Daggitt: Implementing refactoring tools for Agda**There are now some relatively large Agda code bases floating about (the standard library itself is now over 80kloc) and consequently the lack of a smarter editing environment for Agda is becoming more of an issue. Tools that would be useful include refactoring support, automatic import suggestions, and redundant import analysis. It would be great if the relevant parts of the community could share their experience on prior attempts to implement similar tools and on what they see as the best way forward is. Tentative suggestions might include extending Emacs mode and/or Atom mode with additional functionality, or implementing the Language Server Protocol and using the functionality in existing editors such as Eclipse.**Thorsten Altenkirch: Fixing cubical**There are some things to do do make cubical working in practice. I hope we can roll out Andrea's implementation of inductive families (this needs some testing). We should integrate Jesper's implementation of a 2-level type theory into the cubical theory (e.g. I should live there) and library. We need some discussion how cubical should look like in the future. This may feed into a code sprint.**Stephan Adelsberger and Anton Setzer: Optimising Agda**- Equality check possible which allows to check 10^(10^10) = 10^(10^10 + 0) in a millisecond using techniques from automated theorem proving
- Brute force guess proofs with parallel cluster

**Stephan Adelsberger and Anton Setzer: Combining Agda with external tools**- Interface which allows to add external tools (e.g. SAT solvers, model checkers, other decision procedures) to Agda, integrating work by Karim Kanso.
- Integration of Lambda prolog with Agda
- SPARK Ada with Agda why3

**Proposer: Title**Explanation.

## Code sprint proposals

List code sprint proposals here.

**Matthew Daggitt: Tactics in the Standard Library**The Standard Library has recently added its first tactics using Agda's reflection framework, and is currently looking for more. This code sprint would firstly be an opportunity for anyone who has developed useful tactics or tactic-related utilities to contribute them to the library. Secondly, those who have some experience developing tactics might be available to provide some pointers to those (such as myself) who are just starting out. People who are interested in taking part in the code sprint: Matthew Daggitt, Jesper Cockx, Tomas Möre, Reed Mullanix, Nils Anders Danielsson.**James Wood: Typed pattern synonyms**Agda's pattern synonyms, introduced by the`pattern`

keyword, are currently untyped. While this is a simple and lightweight solution, it causes several problems:- Normal constructors can be overloaded based on their type. This is very useful when working with two similarly structured types at the same time, like
`List`

and`All`

. But pattern synonyms have no type, so cannot be overloaded like this. - When a pattern can be rewritten using a pattern synonym, Agsy tends to do this eagerly. Often this happens as a coincidence, perhaps due to overloading of constructors, producing a confusing and morally ill typed result.
- There is no sanity checking of pattern synonyms. Pattern synonyms may have a definition that is ill formed, and there is no warning of this.
- There is no interactive editing support when writing a pattern synonym. Standard practice is to define a function of the desired type, then delete the type and add the word
`pattern`

. - Pattern synonyms are not self-documenting, because we had to delete the type declaration.
- Pattern synonyms cannot handle implicit arguments well. With types, it would make sense to solve implicit arguments like normal for constructors and functions.

- Normal constructors can be overloaded based on their type. This is very useful when working with two similarly structured types at the same time, like
**Thorsten Altenkirch : An Agda REPL integrated in emacs**When teaching with agda I miss an agda top level where I can evaluate expressions interactively. C-c C-n doesn't really cut the ice! Hence I would like to resurrect interactive agda and integrate it into the emacs mode (maybe also for other editors). That is I would like to press some keys and the current buffer is loaded into interactive agda which shows up in a different buffer. I need somebody who knows emacs lisp and maybe has some experience with the agda mode.**Thorsten Altenkirch: Destructors for indexed records and coinductive types**I would like to be able to write:

record Vec (A : Set) : ℕ → Set where coinductive destructor hd : {n : ℕ} → Vec A (suc n) → A tl : {n : ℕ} → Vec A (suc n) → Vec A n

**Anton Setzer: A Mechanism for the flexible addition of external tools to Agda**In his PhD thesis Karim Kanso created a mechanism in Agda for flexibly adding builtins to Agda. This was used integrate a SAT solver and a model checkers into Agda by overriding an existing but inefficient decision procedure in Agda by an external tool. Such a mechanism would allow in general to add external tools at type checking to Agda. Karim used this in order to verify a real world railway interlocking system in Agda. He proved specific properties of the concrete interlocking systems using the external tools and carried out more generic proofs in standard Agda. Karim created a fork of Agda which has never integrated into main Agda, and this fork would need to be updated. I'm myself an experienced user but not an implementer of Agda and would need some help with this. Because of my schedule week 2 would be more suitable for this project but I would of course support those wanting to start with this project earlier. Karim Kanso wrote when contacted : "The good news is that it does not appear to have diverged too much. All the needed insertion points remain and look very similar, however, inevitably some of the function names, types and modules have changed. This is where the effort needs to be spent." Karim, who has not been working with Agda or Haskell for some time, wrote as well that he would be happy to attend for a focused session, such as a discussion related to external tools to provide any input. There is a git repository with the Agda fork of Karim, the PhD thesis by Karim can be found here, and here you can find a publication by Karim and myself about this project.