Agda Implementors' Meeting XXXIX

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

Table of contents
Overview Full Program Talk Proposals Discussion Proposals Code Sprint Proposals Organisation Location Restaurants Places to visit International Travel Registration Accommodation Excursion Organising Committee Participants Wrap-up Notes

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 Bullet 1 Bullet 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)

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.

Codesprint Template with webpage Example

Proposer

Item 1 Subitem 1 Subitem 2 Item 2 Subitem 1 Subsubitem 1

Injectivity in cubical

Thorsten Altenkirch

Can we automatically create injectivity and non-confusion?

Cubical reflection

Marcin Jan Turek-Grzybowski

Continuuing work on solver from Cubical reflection machinery and Solvers for Paths (and related agda PRs), I will attempt exposing face constraints of holes in macros.

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

• std-lib-meta

backends

James Chapman

Lambda box/agda2rust

Title

Author

Description

Organisation

---

---

Location

---

The meeting will take place at (Chalmers Johanneberg Campus), OOTO Room 4 (ground floor).

Restaurants

• The Bishop's Arms Park Avenue

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
  • Getting to Gothenburg
• 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
  • Ferry (e.g. from Kiel)
  • Train, e.g. SJ, DB, ...
  • Coaches, e.g. Flixbus, bus4you, ...

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

---

• E.g. Hotel Panorama in walking distance, our usual recommendation.

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:

---

Powered by PmWiki