The 36th Agda Implementors' Meeting will take place in Delft, Netherlands from 10 May 2023 to 16 May 2023. It will be hosted at the social hub situated in Delft city center, just in front of the train station. It will be possible to attend the morning talks online, but the rest of the meeting is in-person only.
| Registration deadline | | : 12 April 2023 (soft deadline) |
| AIM XXXVI | | : 10 May 2023 - 16 May 2023 |
Program
Planning
| Wednesday, 10 May (Meeting room 1+2) |
|---|
| 09:30 | Welcoming |
| 10:15 | Coffee break |
| 10:30 | Talk : Guillaume Allais, Seamless, Correct, and Generic Programming over Serialised Data |
| 11:15 | Coffee break |
| 11:30 | Discussions |
| 12:30 | Lunch |
| 14:00 | Code Sprint |
| 16:00 | Coffee break |
| 16:15 | Wrap up meeting |
| Thursday, 11 May (Meeting room 1+2) |
|---|
| 09:30 | Talk : Sára Juhošová, On the Usability of Agda2HS |
| 10:15 | Coffee break |
| 10:30 | (talk by Ivar moved to Friday) |
| 11:15 | Coffee break |
11:30 12:00 | Talk : Andre Knispel, Syntactic metaprogramming |
| 13:00 | Lunch |
| 14:00 | Code Sprint |
| 16:00 | Coffee break |
| 16:15 | Wrap up meeting |
| Friday, 12 May (Meeting room 1+2) |
|---|
| 09:30 | Talk : Ivar de Bruin, Improving Agda’s module system |
| 10:15 | Coffee break |
| 10:30 | Talk : Quentin Canu, A Formal Disproof of the Hirsch Conjecture |
| 11:15 | Coffee break |
| 11:30 | Discussions |
| 12:30 | Lunch |
| 14:00 | Code Sprint |
| 16:00 | Coffee break |
| 16:15 | Wrap up meeting |
| Saturday, 13 May (Meeting room 1+2) |
|---|
| 10:00 | Talk : Jesper Cockx |
| 11:00 | Talk : James Chapman, private ledgers |
| 12:00 | Lunch |
| 14:00 | Happy Hacking |
| Sunday, 14 May |
|---|
| all day | Excursion to Scheveningen + Meijendel nature reserve |
| Monday, 15 May (Meeting room 1+2) |
|---|
| 09:30 | Talk : Orestis Melkonian, Program logics for ledgers |
| 10:15 | Coffee break |
| 10:30 | Talk : Marcin Jan Turek-Grzybowski, CubeViz2: An Interactive Tool for Developing and Visualizing Cubical Agda Proofs |
| 11:15 | Coffee break |
| 11:30 | Discussions |
| 12:30 | Lunch |
| 14:00 | Code Sprint |
| 16:00 | Coffee break |
| 16:15 | Wrap up meeting |
| Tuesday, 16 May (Meeting room 1+2) |
|---|
| 09:30 | Talk : Wouter Swierstra, |
| 10:15 | Coffee break |
| 10:30 | Talk : Joey Eremondi, On The Design of a Gradual Dependently Typed Language for Programming cancelled |
| 11:15 | Coffee break |
| 11:30 | Discussions |
| 12:30 | Lunch |
| 14:00 | Code Sprint |
| 16:00 | Coffee break |
| 16:15 | Wrap up meeting |
Talks
| Program logics for ledgers |
|---|
| Orestis Melkonian |
| Distributed ledgers nowadays manage substantial monetary funds in the form of cryptocurrencies such as Bitcoin, Ethereum, and Cardano. For such ledgers to be safe, operations that add new entries must be cryptographically sound—but it is less clear how to reason effectively about such ever-growing linear data structures. This paper views distributed ledgers as computer programs, that, when executed, transfer funds between various parties. As a result, familiar program logics, such as Hoare logic and separation logic, can be defined in this novel setting. Borrowing ideas from concurrent separation logic, this enables modular reasoning principles over arbitrary fragments of any ledger. All the results presented in this paper have been mechanised in the Agda proof assistant and are publicly available. |
| Seamless, Correct, and Generic Programming over Serialised Data |
|---|
| Guillaume Allais |
| In typed functional languages, one can typically only manipulate data in a type-safe manner if it first has been deserialised into an in-memory tree represented as a graph of nodes-as-structs and subterms-as-pointers. We demonstrate how we can use QTT as implemented in Idris 2 to define a small universe of serialised datatypes, and provide generic programs allowing users to process values stored contiguously in buffers. Our approach allows implementors to prove the full functional correctness, in a correct-by-construction manner, of the IO functions processing the data stored in the buffer. |
| Master Thesis: Improving Agda’s module system |
|---|
| Ivar de Bruin |
| Over the past few month I have investigated the possibility of switching Agda to a structured module system to improve its performance. To do this I have created a number of different versions of a module system for a simplified version of Agda and analysed their performance in a variety of scenarios. During this talk I would like to show what I found and explain what I believe still needs to be done before any refactor can be performed. |
| Master Thesis: On the Usability of Agda2HS |
|---|
| Sára Juhošová |
| (on Wednesday or Thursday) |
| For my Master Thesis, I've been working on improving Agda2HS and investigating whether and how we can make it more usable. I'd like to use this talk to discuss what I've changed and what I've found during the user study. |
| Phd Thesis: On The Design of a Gradual Dependently Typed Language for Programming |
|---|
| Joey Eremondi |
| Short Abstract: I describe a design for gradual dependent types, a system by which dependently typed programs can be run when missing parts of types, proofs, or programs. This serves a dual purpose. First, it reduces the barrier to entry for dependent types, making it easier to migrate code to use dependently typed languages, and allowing indexed types to be safely used even when type or proof information is missing. Second, it gives dynamic semantics to the typed holes that are already found in modern languages, so programs can be safely run when holes are missing, providing the programmer with useful information of what terms should fill the holes. In the talk, I present a vision for what programming with gradual dependent types could look like, along with technical challenges that arise with it and solutions to some of these challenges. |
| A scope API based on proof-relevant separation algebra |
|---|
| Jesper Cockx |
| Short Abstract: Most implementations and formalizations of dependently typed languages (including Agda) use de Bruijn indices or variants thereof for representing variables. However, this requires low-level fiddling with indices for many operations and can thus easily lead to bugs. In this talk I will present a work-in-progress API for dealing with scopes and binders that is based on Arjen Rouvoet's *proof relevant separation algebras*, ternary relations that determine how names in one scope are distributed over two others. The goal of this project is to create a safer and more convenient way to define well-scoped syntax for projects such as Agda Core and agda2hs. |
| A Formal Disproof of the Hirsch Conjecture |
|---|
| Quentin Canu |
| The purpose of this presentation is to describe our work on the formal verification of a counterexample of Santos et al. to the so-called Hirsch Conjecture on the diameter of polytopes (bounded convex polyhedra). In contrast with the pen-and-paper proof, our approach is entirely computational: we implement in Coq and prove correct an algorithm that explicitly computes, within the proof assistant, vertex-edge graphs of polytopes as well as their diameter. This algorithm requires only elementary computations, such as matrix multiplications or set manipulation, which are implemented using efficient data types as persistent array. We emphasize on the Coq reduction mechanism used to execute the algorithm, and on data refinement techniques used to prove it correct. |
| CubeViz2: An Interactive Tool for Developing and Visualizing Cubical Agda Proofs |
|---|
| Marcin Jan Turek-Grzybowski |
| CubeViz2 is a tool designed to support the development process and improve the readability of cubical Agda code. Building upon earlier work in Elm , the current version is implemented in Haskell and provides integration with both Emacs and the Agda compiler. In this talk, I will offer a brief overview of the implementation, share some examples, and invite feedback from the Agda community. The project has reached an early stage of release and can be utilized with a relatively straightforward setup. Furthermore, we will touch upon some initial modifications made to the Agda compiler to enable integration with CubeViz2, and seek advice on how to align these changes with ongoing Agda development. As a bonus, an interactive activity will be incorporated into the talk, seeking to provide an enjoyable and informative experience for the audience. :) |
| Syntetic MetaProgramming |
|---|
| Andre Knispel |
| In this talk, I will be presenting my solution for the problem that proof assistants are sometimes inflexible and always incredibly large: syntactic metaprogramming. While metaprogramming support is a common feature of proof assistants for the development of tactics (most notably in Coq and Lean 3), if given sufficient power over syntax it can also be used to implement essentially every feature of the surface language. Examples of this are the module system, unification/inference, datatype definitions and of course notations for terms and literals. The reference system that implements this style of metaprogramming is written in Agda and is about 3k LOC. All the above examples have been implemented as metaprograms. |
Discussion Proposals
| Something to talk about |
|---|
| Agda Wiki |
| Lorem ipsum dolor sit amet, consectetur Lorem ipsum dolor sit amet, consectetur Lorem ipsum dolor sit amet, consectetur Lorem ipsum dolor sit amet, consectetur Lorem ipsum dolor sit amet, consectetur Lorem ipsum dolor sit amet, consectetur Lorem ipsum dolor sit amet, consectetur Lorem ipsum dolor sit amet, consectetur |
| Something to talk about |
|---|
| Agda Wiki |
Code Sprint Proposals
| agda2train |
|---|
| Orestis Melkonian, ... |
| I have been prototyping a simple Agda backend for generating training data for machine learning purposes: https://github.com/omelkonian/agda2train. It "compiles" Agda programs to training data, by traversing the (typechecked) internal syntax and outputting for each possible hole the current context, its type and the term that filled it in. I would like to discuss opportunities for appropriating this tool for other non-ML purposes (e.g. implementing type-on-hover), discuss backend design/implementation issues (e.g. making `checkInternal` more robust, reverting the projection-like optimisation, etc..), as well as investigate how to get the same information on the usage side (i.e. on Emacs, outside the backend). This can act either as a code sprint and discussion, depending on other people's interest. |
| multiple |
|---|
| James Chapman, ... |
| agda2rust backend; extending schmitty to support model checking; extending agda2hs to gadts; extending agda2hs to support compilation of propositions to quickcheck properties; supporting the development of zero knowledge curcuits/proofs |
| Binary distributions |
|---|
| Andreas Abel |
| Various smaller ideas: make pre-build binaries avaialbe to search for bugs easier; improve distributions of agda, make binary distributions avaible; make standard library easier to install; imporve CI experience for Agda |
| Agda base library |
|---|
| Felix Cherubini |
| Create a standard library for naturals, lists, functional data structures, reflections since everyone seems to reinvent it. |
| https://github.com/agda/agda-base |
| Make some tactics |
|---|
| Andre Knispel |
| we have monoid and semiring (?) solver, but we don't have anything that handles cumulativity |
| Squash a bug in the PR |
|---|
| Marcin Jan Turek-Grzybowski |
| There's a pre-existing PR (link?) that has an emacs-related bug, needs help fixing |
| Visual tools for Agda |
|---|
| Marcin Jan Turek-Grzybowski |
| There's some pre-existing work (link?) that is based on a fork of Agda. Either migrate it to master or move to reflection API |
| Experiments with ChatGPT |
|---|
| Marcin Jan Turek-Grzybowski |
| There's a small experiment akin to what Orestis have. |
| Migrate code used in the Idris talk to Agda |
|---|
| Guillaume Allais |
| Migrate the code to do some benchmarks. |
| Finish the opaque implementation |
|---|
| Amélia Liao & Jesper Cockx |
| |
| Polarity annotation and agda2hs bug squashing |
|---|
| Lucas Escot |
| |
| Implement Ivar's thesis |
|---|
| Bohdan Liesnikov |
| |
| Fix occurs-check performance issues |
|---|
| Jesper Cockx |
| |
| Less instantiation of metas |
|---|
| Jesper Cockx |
| There's now an option to avoid as many instantiations during serialization. Can we try avoiding doing as many instantiations as we do now during type-checking? There's already some work on it https://github.com/agda/agda/issues/3094 |
| Programmable unification |
|---|
| James McKinna |
| Implement programmable unification where the user knows something is injective, but the conversion checker isn't aware of it. The Injectivity pragma impacts only pattern-matching. Lossy unification does this, but one would want something more granular. https://github.com/agda/agda/issues/6546 |
| Something doable or not |
|---|
| Agda Wiki |
| Lorem ipsum dolor sit amet, consectetur Lorem ipsum dolor sit amet, consectetur Lorem ipsum dolor sit amet, consectetur Lorem ipsum dolor sit amet, consectetur Lorem ipsum dolor sit amet, consectetur Lorem ipsum dolor sit amet, consectetur Lorem ipsum dolor sit amet, consectetur Lorem ipsum dolor sit amet, consectetur |
Organisation
The meeting will be hosted by Jesper Cockx.
The meeting will last 7 days from Wednesday 10th May – Tuesday 16th May, including one excursion day on Sunday 14th May.
Venue
The Agda Implementors' Meeting XXXVI will take place at The Social Hub located in the center of Delft in front of the train station.
- Address: Van Leeuwenhoekpark 1 2611 DW, Delft
- Room: Meeting Room 1+2
Travel
Getting to Delft
The city of Delft is located between The Hague (Den Haag) and Rotterdam.
The closest airports to Delft are Amsterdam Schiphol Airport (AMS) and Rotterdam-The Hague Airport (RTM).
- Schiphol Airport has train connections to Delft (usually every 15 minutes a direct connection). For some connections you need to change at Leiden.
- Rotterdam-The Hague Airport has bus connections to Rotterdam. Rotterdam has train connections to Delft (usually every 10 minutes or less there is a direct connection).
You can also reach the cities Amsterdam and Rotterdam by high-speed trains from:
- Germany and Switzerland (ICE International via Utrecht)
- Belgium and France (Thalys)
- England (Eurostar)
Delft has two train stations:
- The main train station “Delft Station” (has frequent Intercity (IC) connections from Amsterdam, The Hague, Rotterdam, and other Dutch cities).
- The smaller train station “Delft Campus Station” (has only Sprinter (SPR) connections, Intercity trains do not stop there).
To determine your route and travel time to (or in) Delft for all public transportation you can use 9292. To determine your train connection and travel time you can use NS.
We recommend to travel to the main train station “ Delft Station”. The meeting venue is located across the bus platforms, once you get out of the main train station you see a tall building in front of you.
It is possible to rent a bike at most bike shops, for example Fietsplus https://goo.gl/maps/DWotyhEo4EXD8Nsk9?coh=178572&entry=tt is close to the station.
Registration
To register, you can fill in the following form and send it to thomas[dot]lamiaux@ens-paris-saclay.fr
You only also directly fill in your name in the section participants.
In which case, you can also directly add a talk / discussion / code sprint proposal by copy and pasting the box examples.
If you can not attend in person, it will be possible to attend online to
the morning talks. You can register via email or directly by adding your name
to the list.
| to: thomas[dot]lamiaux@ens-paris-saclay.fr
|
| object: Registration form for Agda Implementors' Meeting XXXVI
|
- Name:
- Online or In person:
- Institution:
- Dietary restrictions:
- If you wish to give a talk:
- Title
- Short Abstract (Optional)
- If you wish to suggest a talk topic:
- Topic
- Short Description (Optional)
- If you wish to suggest a code sprint:
- Proposal
- Short Description (Optional)
- Other comments:
|
There is no registration fee. Transportation, accommodation and meals are to be covered by the participant.
Thanks to our sponsors we can provide some travel and accommodation funding for students and underprivileged groups who want to attend the meeting. To apply send an email to Jesper.
The participation in the event itself is free of charge.
Accommodation
We recommend that you stay at The Social Hub. This hotel is the same location where the Agda Implementors Meetings will take place this year. We pre-booked a block of 10 rooms. In order for you to book one of these rooms, please use this link. Note that the hotel rooms are on a first come first serve basis. Once you get out of the main train station " Delft Station" The Social Hub is the tall building right in front of you, across the bus platform.
Other conveniently located hotels in Delft include Ibis Styles Hotel, Hotel Grand Canal, Hotel Royal Bridges.
Restaurants
Below is a list of recommended restaurants. There are lots of other places in Delft to explore, if you find a good one feel free to add it to this list!
Cheap bites (< 10 euro):
Good quality:price ratio (10-20 euro):
Something a bit more fancy (> 20 euro):
Beers & Bites:
Excursion
On Sunday, we will take the tram from Delft to Scheveningen, and from there hike to the Meijendel nature reserve. We meet at 10:00 at the tram stop next to Delft central station, or at 11:00 at the Zwarte Pad stop in Scheveningen. Trams go every 15 minutes, we plan to take the one at 10:13. If you do not have a Dutch public transit card, the cheapest ticket is 8€ for a day ticket, which you can buy via the HTM Ticket App or at the station. Detailed information on the tram can be found here: Tram from Delft to Zwarte Pad.
There are many options for hiking on the beach and in Meijendel, we propose this 13.5km round trip. You can get Dutch pancakes for lunch at Boerderij Meijendel (about halfway the hike), or bring your own picnic.
Participants
Attending in person
- Lucas Escot
- Wouter Swierstra (may not be there all days)
- Nathan van Doorn
- Jesper Cockx
- Bohdan Liesnikov
- Sára Juhošová (not all days)
- Arthur Adjedj
- Casper Bach Poulsen (not all days)
- Orestis Melkonian (arriving late on Wed 10th, departing early on Tue 16th)
- Guillaume Allais
- Ivar de Bruin (not all days)
- Peio Borthelle
- Andre Knispel
- Marcin Jan Turek-Grzybowski
- Joey Eremondi
- Lucas Holten
- Felix Cherubini
- Jonathan Coates
- Quentin Canu (Wednesday - Friday)
- Amélia Liao
- James McKinna
- Niels van der Weide (only 15 and 16 May)
- Andreas Abel
- James Chapman (arriving Wednesday 10 May AM)
Attending online
- Thomas Lamiaux
- Liang-Ting Chen
- Nigel Burke
- John Leo
- Oskar Eriksson
- Matthew Daggitt
- (your name here)
Sponsors
Huge thanks to our sponsors:
Wrap-up Notes
Wednesday 10 May
- James (agda2rust): Currently reading the agda to rust student report.
- Andreas (binary distribution): Figuring things out with Wen's action. The question is whether we can keep the current deploy action, which some people currently rely on (maybe?).
- Felix (agda-base): Repo created! Some basic stuff copied from the std-lib, already some (naming) conventions are being discussed.
- Andre (metaprogramming): Just idea gathering for now.
- Marcin: Working on the existing PR. Clearer idea on how to work with cubical formatting.
- Guillaume (serializing): Further porting to Agda. Unsafe views are currently being defined.
- Amy and Peio: Currently fixing the termination checker to (hopefully) allow impredicative (S)Prop.
- James and Nathan: Some work on std-lib PRs.
Thursday 11 May
- Amy (opaque): unsatisfied with the current design, Amy is currently fixing it with Jesper while coming up with a better design.
- Andreas: Looking through issues towards 2.6.4, ideally a release before summer.
- Bohdan: Currently looking into issue #6541.
- Orestis & Andre (stdlib-meta): In progress merging Orestis's and Andre's prelude, going along.
- Felix (agda-base): More aggressive copying from stdlib (and stdlib-meta!), the reflection primitives from the stdlib aren't very satisfying.
- Marcin: Making progress on the PR. More cubes.
- Guillaume (serializing): Ported enough to Agda so that it can read binary files. Playing with agda2hs (there's a new PR: https://github.com/agda/agda2hs/pull/177), reviewing PRs for the stdlib.
- Jonathan: ???
- Nathan & James: Going through more stdlib PRs (#1928, proof of the binomial theorems, finally).
- Peio & Lucas: We have a basic understanding of the analysis Coq does on inductive datatypes. But Coq rejects too much strictly-positive datatypes than we can afford, so we don't have a full solution yet. Started hacking.
- James Chapman: Reflection & Schmitty discussion. With Lucas Holten, got agda2rust to compile and work. Contacting the student to know about licensing.
- Lucas Holten: Working on examples for his thesis, gathered some info about conversion-checking.
- Jesper: support. Started looking into performance regression with the new typed occurs-checker. Will try not reducing the types as much.
Friday 12 May
- Andreas: Wants to work on adding PropOmega. But first some refactoring to collapse Type, Prop, and SSet into a single constructor with a parameter, internally.
- Orestis & James C: Mostly discussions on model-checking, trying out some existing tools (Kind2 model checker). Also a discussion on next steps for agda2hs.
- Andre: Spent all day refactoring stdlib-meta. Surprisingly, it seems to work well with cubical code.
- Felix: Trying to use tactics from the 1lab in cubical.
- Peio & Lucas: Trying to extend Coq's representation of inductive recursive positions to fit Agda's more permissive datatypes (non-homogeneous parameters may be considered strictly-positive by Agda, never by Coq). Considering giving up on this, maybe implement the restricted check that mimics Coq.
- Marcin: Integrating computer algebra system with Agda. Added a way to parse surface-level syntax in the reflection API, [[https://github.com/agda/agda/pull/6629|new PR open]. The motivation for this work is gonna be showcased tomorrow!
- James M & Nathan: Spent the day on closing 3 other PRs. Nathan made some progress on the parity theorem for permutations.
- Guillaume: Using reflection to grab files at compile time, and have well-typed templates at compile-time.
- Jonathan: Still working on the builtins PR.
- Amy: More progress on the opaque PR, fighting the CI.
- Jesper: Worked on a PR to always use the fast reduction engine. This should help improving the performances of the typed occurs checker perf regression. + Slides.
Monday 15 May
- Guillaume: got the templating engine working in Agda! It runs
cat at compile time using Wen's `execTC`, to retrieve a (mustache) template and typecheck it against whichever data is applied to it. With some decent error messages generated. Next up: conditional computations in the stdlib?
- James M:
reveal and inspect have finally been deprecated in the stdlib.
- Nathan: more work on permutation theorem.
- Amy: Small optimization to hcomp for datatypes is turning into a complete rewrite. Implemented a check for ignoring
Prop in termination-checking. You can no-longer recurse on Prop (only). Helped Andre implement "injective for unification" pragma. Some improvements in the documentation of unfolding.
- Marcin: Got some advice from Felix for a PR on cubical-agda. Working on a wrapper around Macaulay2?
- Lucas: Removed a bug with polarity annotations where metas are created without any polarity restrictions. Amy gave the trick of instantiating when re-typechecking using the internal typechecker.
- Andre: Worked on the pragma for injective for unification. Writing some documentation. More (cleanup) work on the metaprogramming library. A showcase to come (tomorrow?).
- Orestis: Prototype working interfacing with Kind2 model-checker withing Agda using
execTC.
- James C: Heard back from the agda2rust student interested in doing more work on the backend. Studying formalizing cryptography protocols and games in Agda, based on some master thesis.
- Felix: Talked to Marcin about how to use external tools from inside Agda. In particular for having a more powerful ring-solver. Currently trying to identify what 1lab relies on that could be part of agda-base.
- Andreas: Added
PropOmega. A lot of time was spent refactoring and fixing corner cases with SSetOmega.
- Jesper: Thinking about having memoized lazy computations for the occurs checker.
- Bohdan: Made a PR.
Tuesday 16 May
- Jesper: Still working on improving the occurs-checker. Uncovered a few bugs in fast reduce.
- Andreas&James C: Doing NbE in the Delay monad. Ported old code to the new(er) stdlib. The project is [[https://github.com/andreasabel/continuous-normalization|live here], showcasing how easy it is to use setup-agda github action to build and deploy agda projects.
- Guillaume: Made more things n-ary in the agda source. Doesn't seem to impact Agda's performance, may increase compile time.
- Marcin: Managed to extract results from Macaulay2 into Agda!
- Jonathan: Compiling Agda to WASM! Too slow to be usable, but very promising.
- Felix: Continued with agda-base. Thinking about splitting agda-base into even smaller fragments (Because 1lab redefines primitives but others don't).
- Andre: Trying to write a tactic for J. Anti-unification. Made the "injective for unification" pragma pass all tests.
- Peio: Playing with well-typed telescopes (again and again).
- Amy: Squashing bugs all day!
