The 39th Agda Implementors' Meeting will took place in Gothenburg, Sweden from Monday 25 to Saturday 30 November 2024. It was be hosted by the
Computing Science Divison, Logic and Types Unit,
Department of Computer Science and Engineering,
University of Gothenburg.
This was the 20th anniversary of Agda meetings, the first took place in Fall 2004 in Gothenburg.
Registration deadline | | : 31 October 2024 (soft deadline) |
AIM XXXIX | | : Mon 25 – Sat 30 November 2024 |
Overview
Monday - Friday we will have talks in the morning, followed by code sprints.
We start at 09:30. On Saturday there will be a social event TBA.
Full Program
Location | OOTO (Webpage) Room 4 (ground floor) (Google Map) |
Zulip | AIM XXXIX Zulip Channel |
Zoom | 689 0840 5131 / aim39, Tuesday: 610 4760 9168 |
Sunday, 24 November |
18:30- | Drop-in dinner at Ölstugan Tullen |
Monday, 25 November |
09:30 | Welcoming |
09:45 | Introduction Round, Talk Schedule |
10:30 | Coffee break |
11:15 | Talk Andre and Orestis, Agda ecosystem overview |
12:30 | Lunch |
13:30 | Talk Andreas, Agda live bugfix sprint attempt |
15:00 | Coffee break |
15:30 | Code Sprints |
16:00 | Talk Bas Spitters |
17:00 | Wrap up meeting |
Tuesday, 26 November |
09:30 | Talk Andre Knispel, Lesson learned from a real-world Agda project Slides |
10:15 | Coffee break |
10:30 | Talk Andre: Agda meta-programming tutorial |
11:00 | Discussions and Code Sprints |
12:30 | Lunch |
13:30 | Talk Nils Anders Danielsson, A formalisation of graded type theory |
15:00 | Coffee break |
15:30 | Code Sprints |
17:00 | Wrap up meeting |
Wednesday, 27 November |
09:30 | Talk Bohdan Liesnikov, Caching Constraints in Type Checking |
10:15 | Coffee break |
10:30 | Discussions and Code Sprints |
12:30 | Lunch |
13:30 | Talk Andreas, Twenty years of Agda Implementor's Meetings |
14:15 | Discussion Typed case trees (Jesper) |
15:00 | Coffee break |
15:30 | Code Sprints |
17:00 | Wrap up meeting |
Thursday, 28 November |
09:30 | Discussions and Code Sprints |
10:15 | Coffee break |
11:15 | Talk Thorsten Altenkirch |
12:30 | Lunch |
13:30 | Code Sprints |
15:00 | Coffee break |
15:30 | Code Sprints |
16:10 | Lean Talk: Jean-Frederic Etienne |
17:00 | Wrap up meeting |
18:30 | Workshop dinner at Ölstugan Tullen |
Friday, 29 November |
09:30 | Talk Ulf Norell, Quasi-quoting in Agda |
10:15 | Coffee break |
10:30 | Discussions and Code Sprints |
12:30 | Lunch |
13:30 | Code Sprints |
15:00 | Wrap up meeting |
16:15 | Coffee break |
16:30 | Wrap up meeting (ctd.) |
19:00 | Bishop's Arms Park Avenue |
Saturday, 30 November |
11:00 | Excursion: Konstmuseum |
13:00 | Grab some lunch at Avenuen |
Talk Proposals
Please add your proposals here by editing this webpage (using the edit button).
You can refer to examples from
previous Agda Implementors meetings.
Talk Proposal Template
|
Presenter 2
|
Paragraph 1
Paragraph 2
|
Being strictly positive with containers |
Thorsten Altenkirch |
I want to discuss what impact recent progress on containers could have on agda. |
Lessons learned from building a large, real-world Agda project |
Andre Knispel |
Building industry projects with various constraints comes with some interesting challanges. I'll be presenting an overview of things that worked and didn't work, from small tricks that make the code just a bit more tidy to large-scale designs and libraries that affect everything. |
Caching type-checking constraints |
Bohdan Liesnikov |
Agda generates and solves constraints during type-checking. Can we cache the solutions to re-use them when the same constraint arises? When can we re-use a solution? What does it mean for two constraints to be the same? WIP, jww Jesper Cockx. |
Verified smart contracts and high assurance cryptographic software (Coq) |
Bas Spitters |
I Monday 4pm |
Lean/Smart contracts (Lean/model checking) (TBC) |
Jean-Frederic Etienne |
I Thursday 4:10pm |
A formalisation of graded type theory |
Nils Anders Danielsson |
A gratuitously general relation type |
William DeMeo |
I could show how to define the most general relation type and some related constructions, like general (algebraic, relational) structure types. |
REL type in agda-algebras |
Title |
Presenter |
Abstract |
Link (optional) |
Discussion Proposals
Please add your proposals here by editing this webpage (using the edit button).
You can refer to examples from
previous Agda Implementors meetings.
Reducing Agda to a small core |
Thorsten Altenkirch |
I want a smaller core than anybody else! |
Proposal Template |
Proposer 1 |
Abstract |
Making friends - Shared front ends, shared backends, shared automation |
James Chapman |
Bridges between systems, using multiple systems in one project, and supporting lightweight automation (testing, model checking, etc) |
Lambda box (hooking into Coq backend to enable verified compilation to WASM, Rust, ...) |
James Chapman/Bas Spitters |
Tuesday 2pm |
Code Sprint Proposals
Please add your proposals here by editing this webpage (using the edit button).
You can refer to examples from
previous Agda Implementors meetings.
Injectivity in cubical |
Thorsten Altenkirch |
Can we automatically create injectivity and non-confusion? |
Agda AI tooling |
William DeMeo |
Develop Agda AI assistant and use Formal Abstracts, Agda Standard Library, and other libraries to train it. |
Caching type-checking constraints |
Bohdan Liesnikov |
I'll continue working on the project during AIM, you're welcome to join me. |
IO open source projects |
James Chapman |
- certifying compilation
- ledger
- Ouroboros Praos
- cryptographic pseudo code
||
IO open source libraries |
James Chapman |
backends |
James Chapman |
Lambda box/agda2rust |
Organisation
Location
The meeting will take place at (Chalmers Johanneberg Campus), OOTO Room 4 (ground floor).
Restaurants
Places to Visit
- City museum: 70 SEK, free with Museum Card (140 SEK)
- Konstmuseum art museum: 70 SEK, free with Museum Card (140 SEK)
- Universeum: science museum, 225 SEK (prebooking)
- TBA
Transportation, local Information, etc.
- General
- Cashless payment is the norm, often cash is not accepted.
- Public transport
- Buses, Trams, and local ferries: Västtrafik
- Tickets through the app or from Västtrafik service stations, or by tapping payment card on card reader onboard
- Bike rental, e.g. Styr och ställ
- Scooters are very popular: Voi, Tier, Lime
International Travel
- Sweden is a Schengen country in the EU. If you are outside of this zone, you may need to apply for a visa, please check.
- Even if you do not need a visa, you need to bring:
- a passport that is valid at least three months after leaving Schengen
- a return ticket that must be valid within 90 days
- a booking confirmation if you are staying at a hotel
- General
- Flying
- Landvetter Airport is well-connected to the major airports of Europe.
- From the airport take the frequent airport bus to Gothenburg (one way ~130 SEK).
Tickets through the app or webpage, from sales machines at the bus stop or from the driver (no cash!).
- There are of course also taxis, but for roughly 4-times the money (e.g. fixed price ~550 SEK).
- Alternatives
Registration
To register, you can fill out the following form and send it to ulfn <at> chalmers <dot> se.
Please advice us if you don't want your name to be added to this webpage.
You can also (if you are okay with your name being public) directly fill your name in the section participants on this webpage using the edit option for it.
In this 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. You can register via email or directly by adding your name to the list.
to: ulfn <at> chalmers <dot> se
|
Subject: Registration for Agda Implementors' Meeting XXXVIII
|
- Name:
- Online or In person:
- Add my name to the Meeting webpage (yes/no):
- Affiliation:
- 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 (e.g. dietary restrictions):
|
Accommodation
Excursion
We visit the Konstmuseum.
We meet Sat 11am in front of the museum on Götaplatsen.
Organising committee
- Andreas Abel, University of Gothenburg
- Nils Anders Danielsson, University of Gothenburg
- Ulf Norell, University of Gothenburg
Participants
Attending in person
- Andreas Abel, University of Gothenburg
- Nils Anders Danielsson, University of Gothenburg (leaving Friday noon)
- Ulf Norell, University of Gothenburg
Andreas Källberg, Chalmers University
- Naïm Favier, Chalmers University
- Marcin Jan Turek-Grzybowski
- Patrik Jansson, Chalmers [arriving Tuesday]
- Oskar Eriksson, University of Gothenburg
- Thorsten Altenkirch, University of Nottingham (arriving Wednesday morning)
- András Kovács, University of Gothenburg
- Andre Knispel, IOG
- Simone Zahn
- Jesper Cockx (leaving Friday morning)
- Orestis Melkonian IOG, (leaving Friday morning)
- Yves Hauser, IOG
- Mario Carneiro, Chalmers
- Peter Dybjer, Chalmers
- Bohdan Liesnikov, TU Delft
- Cas van der Rest, IOG
- Felix Cherubini, University of Gothenburg
- Lucas Escot, TU Delft / IOG (?)
- James Chapman, IOG
- Javier Diaz, IOG
- Ramsay Taylor, IOG
- Ana Pantilie, IOG
- William DeMeo, IOG
- Shin Hyeyoung
- Joosep Jääger, IOG
- Miëtek Bak
- Denis Firsov, IOG (arriving Monday AM)
- Carlos Tomé Cortiñas
Attending online
Wrap-up Notes
- Andreas Abel: help with Agda & getting code sprints started
- Nils Anders Danielsson: a formalization of a core of type theory
- James Chapman:
- Ulf Norell: Monad monomorphication
- Peter Dybjer:
- Mietek Bak: improve the emacs interface, improve JS backend, print Agda T-Shirts
- Andras Kovacs: improving the performance of the operator parser (overheads in the scope management)
- Cas (IOG):
- Simone:
- Andre Knispel (IOG): finish old code sprints, simplification tactics
- Orestis Melkonian (IOG): backends: agda2hs, lambda-box (Bas Spitters), agda2rust prototype, agda2train (AI)
- Carlos Tome:
- Javier (IOG): formalizing consensus protocols
- Yves Hauser (IOG): formalizing consensus protocols
- Alex (Chalmers): learn Agda
- Marcin: improve reflection
- Anna (IOG): agda2hs, learn about Agda implementation
- Ramsey Taylor (IOG): certified translation, Agda syntax
- William De Meo (IOG): AI tooling (models), discrete probability theory, measure theory
- Hyeyoung Shin: learn more Agda
- Felix Cherubini: formalization in Agda, cubical Agda library
- Bogdan: WIP talk on constraints (formalization)
- Oskar Eriksson: formalization of type theory in Agda
- Jesper Cockx: let-bindings in Agda internal syntax, agda2hs
- Joosep Jääger (IOG): conformance testing Agda<->Haskell
Plenum:
- Reflection (meta-programming) tutorial (Andre)
- Bugfix-sprint (Andreas)
- Typed-case trees (Jesper)
- Formalization of type theory (Nisse)
- Agda ecosystem (Andre and Orestis, 11am)
- ? lambda-box intro (Bas, Tue 2pm)
Interest groups:
- Certifying compilation (Agda as library): Anna, Ramsay, Jesper, Cas, Orestis
- AI-techniques: William, Orestis, Marcin, Andreas, Mietek, Javier
- agda2hs: Orestis, Jesper, Cas, Andreas, Anna
- lambda-box backend (MetaCoq intermediate language): James, Alex, Andre, Orestis, Carlos, Bas, Anna, Cas
- Formalization of type theory (Agda core, MLTT in Agda); correctness of agda2hs, featherweight Haskell: Mietek, William, Nils, Oskar, Orestis, Anna, Andras, Peter
- Agda ecosystem (open source Agda libraries extending the standard library): Andre, Orestis, Javier, Yves, Alex, Andreas
- Reflection (meta-programming): Andre, William, Javier, Yves, Anna, Ramsay, Mietek, Joosep, Cas, Marcin
- Performance of Agda: Andras, Andre, Mietek, Bohdan, Joosep, Ulf, Jesper, Andreas
Wrap up Monday:
- Andreas: clean up agda organization
- Cas: starting to formalize relations and extracting computable functions
- Mietek: mechanized intuitionist e.g. Martin-Löf, Axiom of Choice
- Andras: picking up the old code sprint
- Jesper: salvaging parts of "let" code sprint, formalizing restrictions of agda2hs in terms of the formalization of erasure (Oskar, Nisse)
- James: discussion on agda2hs and erasure (also Peter, Nisse, Oskar, Orestis)
- Peter: discussion with Thierry about Mietek project of formalizing classic TT papers
- Yves, Javier: discussion about formalizing consensus protocols
- Orestis: discussions... e.g. lambda-box
- Andre: looking into bug in agda-stdlib-meta
- Joosep: looking into meta-programming
- William: discussion with Marcin: interfacing ChatGPT with Agda; revive Universal Algebra library
- Ramsay, Anna: serialization
- Marcin: reflection: producing strings from macros rather than reflected syntax
- Denis Firsov (IOG)
- Bohdan: preparing the talk
- Ulf: discussed new approach to monad monomorphisation with Jesper
Wrap up Tuesday/Wednesday:
- James: discussion about lambda-box (w Bas, Orestis, Carlos) & ouroboros praos
- Nisse: w Jesper: proving correctness of agda2hs: extracting to a simply typed language (using logical relation) from a dep. typed language with erasable dependencies
- Jesper: PR with refactorings from the let-binding code sprint; discussion about typed case trees (w Mario); discussion about the module system: write concrete proposal
- Javier (w Yves): proving safety and liveness of the ouroboros praos consensus protocol; (w Andre): implementation of a simplification tactic
- Andre: fix bug in show instance derivation meta-program; working on the simp tactic
- Mario: discussions with people: typed case trees, agda core proof export
- William: refactor Agda Universal Algebra library to work with latest std-lib; (w Marcin): testing interface with ChatGPT to fill holes
- Marcin: interaction tactics that calls ChatGPT iteratively on goal; needs PR change in catchTC (reflection API); reflection API extension: get name of the current file
- Mietek: organized T-shirts: 50 will be available, can pay to Felix; will put up web-page for post-workship orders
- Andras: minor progress on extending the scope checker with more information
- Oskar: working on the formalization of graded type theory
- Bohdan: (w Orestis, Carlos, Cas) kick-started lambda-box backend
- Orestis: (w Jean-Philipp): revived PR 7010 about backend-specific interaction commands
Final wrap-up (Fri): Demos:
- Ulf (w Jesper): restructuring TCM and ReduceM using a Capabilities parameter and capabilities type classes that can provide e.g. different implementations of MonadMetaSolver to get the functionality of PureConversionT
- Carlos (w Orestis, Cas, Alex, Bohdan): lambda-box backend early prototype
- Marcin (w William): a yolo! tactic that sends context+type (and in successive attempts the error message) to ChatGPT (gpt-4o-mini, gpt-4o, o1-preview)
- Bohdan (w Jesper, Mario): double checker for compiled clauses WIP
- Yves (w Javier, James, William): formalizing the safety and liveness of the ouroboros-praos consensus protocol in Agda
- André: a meta-program for "rewrite": replacing the "rewrite" by a tactic
- Ana: printing certificates for compiler stages in Agda-recheckable form / independently-checkable Agda proofs (de Bruijn criterion / double-checker)
- Mietek: non-profit T-Shirt sale
TBA
- Monday:
- Tuesday:
- Wednesday:
- Thursday:
- Friday: