Main /
\ Main

Agda Implementors' Meeting XXXVIII

The 38th Agda Implementors' Meeting will take place in Swansea, United Kingdom from Monday 13 to Saturday 18 May 2024. It will be hosted by the Theoretical Computer Science Research Group, Department of Computer Science, Swansea University

Registration deadline : 14 April 2024 (soft deadline)
AIM XXXVIII : Mon 13 – Sat 18 May 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 an excusion into the Gower Peninusula, which was UK's first Area of Outstanding Natural Beauty.

Full Program

LocationSwansea University Bay Campus, Computational Foundry, Building 11 on Bay Campus Map
ZulipAIM XXXVIII Zulip Channel
Sunday, 12 May
18:30Possibilty to join for Dinner at Ask Italian, 6 Wind Street, Swansea, SA1 1DF https://www.askitalian.co.uk (No table booking required)
Monday, 13 May
Main room 401, Breakout room from 11:00: 101 Theory lab 209
09:30Welcoming
09:45Talk Andre Knispel: Universal Composability is a Graded Kleisli Category
10:30Coffee break
11:00Introduction Round and Introduction to Code Sprints
11:45Code Sprints
13:00Lunch (room 401)
14:00Code Sprints
14:00Optional Talk Arved Friedemann: Introduction to Agda for Newcomers (Theory lab 209)
15:30Coffee break
15:45Code Sprints
17:00Wrap up meeting
Tuesday, 14 May
Main room 401, Breakout room from 12:00: 101
09:30Talk Thorsten Altenkirch: Coinduction in cubical Agda
10:15Coffee break
10:30Discussions and Code Sprints
13:00Lunch (Crucible (CF109), 1st floor)
14:00Code Sprints
16:00Coffee break
17:00Wrap up meeting
Wednesday, 15 May
Main room 102 (not 11:30 - 14:00, use 101 and Crucible (CF109) during that time), Breakout room from 9:00: 101
09:30Talk Ulf Norell: War stories from the trenches -- using Agda in Industry (Room 101)
10:15Coffee break
10:30Discussions and Code Sprints (CF101 and Crucible) (Switch to Room 102)
13:00Lunch (Crucible (CF109), 1st floor)
14:45Code Sprints
15:30Coffee break
15:45Code Sprints
17:00Wrap up meeting
Thursday, 16 May
Main room 401, Breakout room from 11:00: 201
09:30Talk Andreas Abel: Type-Based Termination Behind the Curtain
10:15Coffee break
10:30Discussions and Code Sprints
13:00Lunch (Crucible (CF109), 1st floor)
14:00Discussion: Arved Friedemann: AGI and optimal Search Strategies for Agda and Type Theory
14:45Coffee break
15:00Code Sprints
17:00Wrap up meeting
19:30Workshop Dinner (Resturant Rasoi https://www.rasoiwaterfront.co.uk/)
Friday, 17 May
Main room 401, Breakout room from 11:00: 201
09:30Talk Peter Dybjer (online): Inductive Definitions, Predicativity, and the Mahlo universe
10:15Coffee break
10:30Discussions and Code Sprints
13:00Lunch (Beach, by the Great Hall)
14:00Code Sprints
15:30Coffee break
15:45Code Sprints
16:30Final Wrap up meeting
Saturday, 18 May
10:00Excursion to the Gower Peninsula, Area of Outstanding Beauty . We will meet at the Morgans hotel in Swansea at 10:00, where we will have cars to take people to the Gower.

We will do a 1-hour walk to a pub at the end of the walk. Given that it's an hour, you might want to bring some water. Also, it may rain, so some waterproof clothing could help.

We expect to be back at around 4/5pm in Swansea. ||

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

--

Coinduction in cubical agda
Thorsten Altenkirch
Cubical agda is good for more than univalence, indeed its set-level features may be its main selling point. I especially like that the asymmetry between inductive and coinductive types is resolved: as we can reason inductively using pattern matching and structural recursion we can reason coinductively using copattern matching and structural corecursion. Alas, the current implementation of the termination checker makes this quite hard sometimes.
Agda code used in the talk
Introduction to Agda for Newcomers
Arved Friedemann
This is a basic introduction into the Agda programming language and proof assistant. We will cover the basic syntax and write our first proofs and programs. We will also have a quick look into Agda's module system, which helps understanding the Agda standard library. It is highly recommended to bring a computer with Agda installed, as this will be an interactive workshop. Installation instructions can be found in the Agda documentation. I personally recommend vscode with the Agda-Mode plugin as a programming environment. The keybindings might have to be fixed using this post. If for some reason Agda cannot be installed, the online tool Agda Pad can also be used.
Using Agda in Industry
Ulf Norell
I talk about a project I'm doing with IOG using Agda to formalise a network protocol and connect the formalisation to a Haskell QuickCheck model that provably generate valid protocol interactions and can be used to test implementations of the protocol. In the talk I show how to do this for a simple toy protocol, but the ideas scale well to more realistic examples.
Type-Based Termination Behind the Curtain
Andreas Abel
I present the work of my MSc student Kanstantsin Nisht on type-based termination for Agda. This work adds a new termination checker to Agda that automatically annotates types with sizes and solves size constraints to generate input for Agda's size-change termination engine. In essence this is a sound and automatic version of termination analysis via sized types.
Talk script and Agda code
Universal Composability is a Graded Kleisli Category
Andre Knispel
In this talk, I will present an abstract categorical setting that can be used to reason about cryptographic protocols based on the Kleisli construction for graded monads. Instantiating it with the right base category and graded monad, the morphisms out of the unit object can be viewed as protocols in a typed version of the (simple) UC framework. Key theorems of the UC framework can then be proven by simple categorical reasoning instead of long-winded constructions of Turing machines.
Inductive Definitions, Predicativity, and the Mahlo universe
Peter Dybjer
We provide a constructive, predicative justification of Setzer's Mahlo universe in type theory. Our approach is closely related to Kahle and Setzer's construction of an extended predicative Mahlo universe in Feferman's Explicit Mathematics. However, we work directly in Martin-Löf type theory extended with a Mahlo universe and obtain informal meaning explanations which extend (and slightly modify) those in Martin-Löf's article Constructive Mathematics and Computer Programming. We also present mathematical models in set-theoretic metalanguage and explain their relevance to the informal meaning explanations.

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

Proposal Template
Proposer 1
Abstract
AGI and optimal Search Strategies for Agda and Type Theory
Arved Friedemann
There is research around the type of type theory that creates a type (in Agda) that represents the valid terms of type theory. Therefore the question arises: Can we build a solver that, for a given type, can give us a term of that type? Of course we know that this can easily be done using the list monad, but especially for type theory there is a much smarter way. If we start with a slow solver for type theory, we could use it to create a solver for type theory that is optimal by some metric (I personally use the maximum likelihood of solving a problem within unknown time bounds), by embedding this question as a type. I'll bring my experience on the topic from my (still ongoing) PhD thesis. I found a way to implement the proof search (theoretically) efficiently using a general solution to dynamic programming, but I would like to discuss how to get all the ideas to actually run in Agda as there have been some yet unsolved technical problems.

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

--

Documentation of Improved Approach for inserting Agda Code into LaTeX
Anton Setzer
Together with Andreas Abel and Stephan Adelsberger we have developed an approach for easy integration of Agda code into LaTeX documents by adding Tags in the LaTeX code from which Lagda files are generated. Our approach uses sed, awk scripts and a Makefile. The first step is to document the existing approach well. We can then discuss whether a more direct support as part of Agda could be established. Added later: A git repository with some draft code is now at https://github.com/csetzer/agdaLatex
(De)serialization overhaul
András Kovács
(de)serialization takes up a lot of time, and the code contains a large amount of uninteresting and error-prone boilerplate. I have fairly concrete ideas for an overhaul that would greatly improve performance, cut out most of the boilerplate and hopefully speed up compile times too, using Typed Template Haskell.
Make cubical agda great again WAS Improve coinduction termination checking
Thorsten Altenkirch
  • Investigate whether we can allow hcomp and transp to be productivity preserving.
  • quotients (QIITs) in practice
  • pattern matching indexed by HITs
  • records with destructors (icebox)
  • local rewriting instead of with [smart case]
  • indexed coinductive types
Installation of Agda for Newcomers
Anton Setzer
Get help in setting up Agda on your computer
Web-based Agda? State of webassembly backend
Binary install with "pip install"
Improving reflection for Cubical Agda. Reflecting partial elements defined by extended lambdas
Marcin
Adding "let" to internal syntax
Jesper Cockx
Agda backends: allow custom ToTreeless pipeline
Orestis Melkonian

When developing backends, the translation from internal syntax to treeless syntax currently only exports toTreeless with a fixed pipeline of optimization passes.

This code sprint is about allowing a backend to tweak that and use a custom pipeline (I already need that in agda2rust), i.e. export a more general toTreelessWith and necessary utilities to build those pipelines.

agda2rust
Orestis Melkonian

I can introduce this new backend with a short demo and see if people are interested in getting involved with my guidance. Tasks:

  • New features:
    • Non-linearity
    • Cover more dependent types
    • Cover more primitives
  • Stabilize codebase, bugfixes, etc.
    • Improve name generation (by taking hints from user-written clauses, etc.)
  • Make the first release on Hackage
  • Migrate under the Agda Github organisation
https://github.com/csetzer/agdaLatex
Ecosystem contributions
Orestis Melkonian
  • Migrate the following user repositories under the Agda organisation:
  • Also bring them up-to-speed with the latest (minor) releases of agda/agda-stdlib
  • Migrate things from my own formal-prelude to stdlib or other appropriate places:
    • deeply personal code sprint, but help would be appreciated!
Language Server for Agda
Amélia Liao and Jonathan Coates
Implementing support for Microsoft's Language Server Protocol for Agda, and integrating it with VSCode and Emacs

Organisation

Location

The meeting will take place at The Computational Foundy, Swansea University Bay Campus, Swansea, United Kingdom.

Please note that there are two main campuses of Swansea University, and the workshop will be held at the new Bay Campus which is to the east of Swansea

  • Address: Department of Computer Science, The Computational Foundry, Swansea University Bay Campus, Fabian Way, Swansea, SA1 8EN

Restaurants

Places to Visit in Swansea

Transportation, local Information, etc.

International Travel

  • Please note that because of Brexit most visitors from the EU will need a passport to enter the UK (National Identity cards are in most cases no longer valid for entry to the UK).
  • Please check the Rules for entering the UK carefully.
  • See as well Guidance for Visiting the UK as an EU, EEA or Swiss citizen
  • General
  • Airports
    • Cardiff Airport is closest, but please check transport to/from it especially for early morning and late night arrivals/departures.
    • Bristol Airport second closest airport (check transport for early morning and late night flights).
    • Heathrow Airport is probably most commonly used airport from Swansea.
      • You can plan your journey directly using Google maps.
      • For trains you can take
        • Elizabeth line to Hayes & Harlington, then change for the Elizabeth line to Reading, and then take the mainline trains to Swansea. To see this option (Anton Setzer's preferred option) you need to choose on the Train journey planner (Journey planner rail) the option "avoiding London" (go for advanced search and look for "Route via/avoid" and then avoid London)
        • More expensive, and sometimes a little bit faster, although in many cases you save only a few minutes: Heathrow Express to London Paddington and then (usually direct) train to Swansea (Journey planner rail)
        • Cheaper: Use National Express, Megabus, or Flixbus to Swansea.
    • Gatwick Airport (a bit longer journey but still well connected)
      • You can plan your journey directly using Google maps.
      • You can take train either via London or (usually cheaper and less stressful) a train which goes to Reading and from there change to Swansea (National Rail Journey Planner; for getting connection avoiding London use advanced search and choose "Route via/avoid" and then avoid London)
      • You can take as well National Express, Megabus, or Flixbus to Swansea. (Possibly directly from Gatwick Airport to Swansea - this is quite a long journey, but usually much cheaper).
    • Other London Airport (Stansted, Luton, London City Airport, London Southend Airport)
      • You can plan your journey directly using Google maps.
      • Usually need to go from there to London
      • Typically quite a long journey (but you might get some cheaper tickets).
      • From Stansted there are direct coaches to Heathrow where you can change for coaches to Swansea.
    • Swansea Airport is only usable for private planes at the moment (we had visitors coming that way).
  • Train to London Eurostar, Rail Europe
  • You can experiment with train to Calais, ferry to Dover, and other ferries from the Continent to Britain.
  • Ferry to Portsmouth from north of France (e.g. Caen, St Malo, Cherbourg, Le Havre)
    • Reasonably good train connection from Portsmouth via Cardiff to Swansea.
  • Coaches to London

Registration

To register, you can fill out the following form and send it to mukeshtiwari <dot> iiitm <at> gmail <dot> com 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: mukeshtiwari <dot> iiitm <at> gmail <dot> com
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:

Accommodation

  • Choosing hotels
    • There are some hotels near the Bay Campus (long and not very pleasant walk or take bus or taxi).
    • We will have dinner in the city center, so it might be more convenient to have a hotel there.
    • Hotels in proximity to Bay Campus (but still needing bus or taxi)

Excursion

On Saturday we will plant to have a walk in the Gower Peninusula, UK's first Area of Outstanding Natural Beauty. The precise route will be decided by our experienced local hikers depending on the weather forecast.

Organising committee

Participants

Attending in person

  • Anton Setzer, Swansea University (second homepage)
  • Mukesh Tiwari, now Swansea University
  • Olga Petrovska, Swansea University
  • Monika Seisenberger, Swansea University
  • Jesper Cockx, TU Delft
  • Arved Friedemann, Swansea University
  • Ulf Norell, University of Gothenburg
  • Marcin Jan Turek-Grzybowski
  • Amélia Liao
  • Jonathan Coates
  • András Kovács, University of Gothenburg
  • Fredrik Nordvall Forsberg, University of Strathclyde [arriving on Monday]
  • Thorsten Altenkirch, University of Nottingham
  • Swaraj Dash, Heriot-Watt University
  • Ulrich Berger, Swansea University
  • Alec Critten, Swansea University
  • Andreas Abel, Chalmers and Gothenburg University
  • Harry Bryant, Siemens Mobility (only Monday)
  • Ian Price, Swansea University
  • Jay Paul Morgan, Swansea University
  • William DeMeo, IO
  • Andre Knispel, IO
  • Orestis Melkonian, IO (Tuesday onwards)
  • Hyeyoung Shin, CVUT
  • Xiaochun Cheng, Swansea University

Attending online

  • Arthur Scott
  • Corey Thuro
  • Fahad Faleh Alhabardi, Swansea University
  • Peter Dybjer, Chalmers University of Technology (Fri only)
  • Miëtek Bak
  • Mark Laws
  • Bohdan Liesnikov (for a few talks)

Wrap-up Notes

Note: we try the template grouped by Code Sprints (easier for people to read). There is still the old one grouped by days below, in case that works better.

Language Server

  • Monday - Amy and Jonathan spent a lot of time trying to get interaction points working with the language server protocol. They're hitting some issues with actions that mutate the program body (such as give/refine), as VS code sends different edits to what Agda is expecting.
  • Tuesday: It's going. Working on a solution to the position mapping problem. Also working on allowing the elaborator to report more than one type error. The challenge is to find safe points where exceptions can be caught and eg a meta can be emitted.
  • Wednesday: Working solution for position mapping, currently committing. Working on the goal display widget as a web app. Thinking about how to embed more semantic information.
  • Thursday: demo! LSP in VSCode, emacs features except case splits.
  • Friday: Mostly a day of fiddling with things, rather than any serious work. We got the language server working with Emacs (eglot and lsp-mode) and NeoVim, both of which only took a couple of lines of code. This is what we were hoping for, but nice to see it pan out.

Let bindings in internal syntax

  • Monday - Jesper is looking at let bindings in the internal syntax. The main problem is we need the value of the let bound variable to be visible in the body, but that requires some major changes to the context, so is proving to be a bit more work than expected.
  • Tuesday: Jesper, Fredrik and Orestis have been making slow progress. Lots of refactoring needed, so far mostly improving artisan uses of de Bruijn variables by using high-level helper functions instead.
  • Wednesday: debugging bugs introduced by yesterday's refactoring.
  • Thursday: Progress: inlining let, helper functions for let-bound variables, found previous bug. Infrastructure mostly.
  • Friday: Largely working on the elaborator. There's some cases they can't handle yet, so have added a flag to handle how they should be handled. Let bindings are preserved all the way though to MAlonzo, which is neat! Currently debugging an issue when looking up let-bound variables during substitution. It's not entirely clear whether putting let-bound variables as a separate constructor was a good idea. It's nice for debugging, but has complicated some of this code.

LaTeX and Agda

  • Monday - Andreas and Anton have been looking at LaTeX, but hit some annoying issues where Agda's style file overrides existing definitions.

    There was some discussion about how best to handle this, Amy suggested that we might want to support alternative environments to just \begin{code} (e.g. minted).
  • Tuesday: Anton reports that it is now running; remains to clean up the code and test it. There will be a git repo, and documentation. (Added after meeting: a draft version of the repo is now available at https://github.com/csetzer/agdaLatex)
  • Wednesday: working on making repository more conventional and cleaning up code. Still on wishlist: creating expressions. Please try it out with @git clone@ and @make@!
  • Thursday: no real progress, live demo and docs in the github repo.
  • Friday: Nothing to report today.

Improved serialisation

  • Monday - András has been looking at a generic serialiser. There's no blocking issues, just lots of busy work.
  • Tuesday: Again great progress. The code is pushing the boundaries of Template Haskell, but in the end it will be really fast. Issues with different versions of GHC will be fixed later.
  • Wednesday: got to the point where we generate some code which is not yet well-typed. Now trying to make it well-typed.
  • Thursday: generated code is now well-typed, starting to debug code execution
  • Friday: Have managed to get the generic serialiser working. We can now round-trip arbitrary ADTs and ints (though not yet strings and other primitives). There are still some issues with hash-consing, the code includes a custom hashtable, and the lookup function is a little buggy.

Cubical and coinduction

  • Tuesday: Experiments with sized types and cubical. The new type based termination checker does not look into Path types. Hacky solutions: You should be able to eliminate transitivity by putting in extra assumptions, or using coinduction directly.
  • Wednesday: had some discussions. Transport can not be in general size-preserving, but hcomp is, which would be sufficient to address transitivity. Proposal: can we integrate it into the new type-based termination checker? An alternative that was discussed is to use sized types, which would require shape irrelevance. Unfortunately, cubical does not support generating transport for (shape-)irrelevant functions.
  • Thursday: no progress, Thorsten played with type-based termination
  • Friday: No progress. Thorsten has found several bugs with type-based termination, so holding off doing any more work here. He and Swaraj have been looking at higher containers.

Reflection for cubical

  • Monday: Marcin has been looking at how we handle reflecting partial element face patterns. We currently return a reflected version of internal syntax, but you then can't reify that back to actual internal syntax. Ideally we'd return some opaque object instead
  • Tuesday: Added missing information to pattern info, so that equals patterns can be be used in reflected syntax. A WIP PR has been created. Simple examples work, but something is wrong with the scope of reflected EqualP patterns. However already the whole cubical library can be checked.
  • Wednesday: Working on reifying pattern info to abstract syntax. Having let bindings in internal telescopes would be really useful.
  • Thursday: in-place substitution for interval variables in patterns. Pretend harder that we don't match on interval variables. There's a bug that's expected to be in compiled clauses.
  • Friday: Marcin has been finished this off. This will be a breaking change to reflection, so will need to update standard library (and anything else using reflection).

Custom toTreeless optimization pipeline

  • Thursday: Orestis opened a PR, but there is still some work to fully consider unused arguments as well (in particular how to control stripUnusedArguments).
  • Friday: PR is merged!

Ecosystem contributions

  • Friday: Orestis opened a PR to agda-stdlib that ports some lemmas about catMaybe/mapMaybe from formal-prelude. Also set up a fortnightly meeting with Andre Knispel to port more stuff from our shared libraries.

Removing MTL

  • Thursaday: Ulf: new code sprint for de-mtl-izing Agda. First question: can we get rid of ReduceM? So far there's not many reason for it to be pure. Motivations for ReduceM? Plan: everything should run in TCM + phantom capabilities.
  • Friday: ReduceM has been removed and replaced with a simple TCM. It's a little slower, as instantiateFull now runs in TCM rather than being a pure function. Now it's mostly the boring work of replacing the TCM types, which is going ... slowly.

Other discussions

  • Monday
    • Thorsten started some discussion about rewrite rules, coinduction and smart and mega withs.
    • Monika reported on the Arved's Introduction to Agda session. It was really helpful, but there is a steep learning curve in getting used to both agda-mode, and Agda itself. It was a useful insight into that don't have to hold you can do proofs incrementally in Agda, rather than having to hold everything in your brain
    • Arved, of course, has been running the intro to Agda course. There was some discussion about whether Agda (especially its syntax) is too powerful, and that can be a hindrance to learning it.

      It would be nice if we could make universe/level polymorphism implicit. Nobody wants to write all the levels out! It should be possible to do something here, but it's not clear if it's going to be impenetrable when it goes wrong. Maybe we could do something Good Enough for the common cases.
  • Tuesday:
    • Ulrich Berger has installed Agda and even run it. Looking at non-strictly positive definitions.
    • Ulf: adding solve instance constraints to reflection. Worked already yesterday, but also want it to play nicely with "noConstraints", which was trickier than expected. Only thing remaining is to make sure that "noConstraints" only means the new constraints generated by the tactic, not any constraints that happen to be floating around from the outside. The test case is written, so now all that remains is to implement the right thing.
    • Arvid: trying to build a general solver. Realised that there is a need to turn a sums-of-products data type into a lattice.
  • Wednesday
    • Ulf: finished adding "noConstraints" primitive to reflection.
    • Orestis & Swaraj: Introduction to agda2rust, getting agda2rust to install with Nix, made some progress to cover more dependent types.
  • Friday
    • Type based termination: Andreas has been looking at the PR, and trying to look into the bugs that Thorsten found.
Edit | History | Recent Changes (all) | Search
Page last modified on May 19, 2024, at 07:37 am
Powered by PmWiki