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


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


LocationOOTO (Webpage) Room 4 (ground floor) (Google Map)
ZulipAIM XXXIX Zulip Channel
Zoom689 0840 5131 / aim39, Tuesday: 610 4760 9168
Sunday, 24 November
18:30-Drop-in dinner at Ölstugan Tullen
Monday, 25 November
09:30Welcoming
09:45Introduction Round, Talk Schedule
10:30Coffee break
11:15Talk Andre and Orestis, Agda ecosystem overview
12:30Lunch
13:30Talk Andreas, Agda live bugfix sprint attempt
15:00Coffee break
15:30Code Sprints
16:00Talk Bas Spitters
17:00Wrap up meeting
Tuesday, 26 November
09:30Talk Andre Knispel, Lesson learned from a real-world Agda project Slides
10:15Coffee break
10:30Talk Andre: Agda meta-programming tutorial
11:00Discussions and Code Sprints
12:30Lunch
13:30Talk Nils Anders Danielsson, A formalisation of graded type theory
15:00Coffee break
15:30Code Sprints
17:00Wrap up meeting
Wednesday, 27 November
09:30Talk Bohdan Liesnikov, Caching Constraints in Type Checking
10:15Coffee break
10:30Discussions and Code Sprints
12:30Lunch
13:30Talk Andreas, Twenty years of Agda Implementor's Meetings
14:15Discussion Typed case trees (Jesper)
15:00Coffee break
15:30Code Sprints
17:00Wrap up meeting
Thursday, 28 November
09:30Discussions and Code Sprints
10:15Coffee break
11:15Talk Thorsten Altenkirch
12:30Lunch
13:30Code Sprints
15:00Coffee break
15:30Code Sprints
16:10Lean Talk: Jean-Frederic Etienne
17:00Wrap up meeting
18:30Workshop dinner at Ölstugan Tullen
Friday, 29 November
09:30Talk Ulf Norell, Quasi-quoting in Agda
10:15Coffee break
10:30Discussions and Code Sprints
12:30Lunch
13:30Code Sprints
15:00Wrap up meeting
16:15Coffee break
16:30Wrap up meeting (ctd.)
19:00Bishop's Arms Park Avenue
Saturday, 30 November
11:00Excursion: Konstmuseum
13:00Grab 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)
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.

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

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.

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:

Page last modified on December 12, 2024, at 10:59 pm
Powered by PmWiki