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

Program

Monday - Friday we will have talks in the morning, followed by code sprints. We plan to 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.

Planning

TBC

Talks Proposals

Please add your proposals here by editing this webpage (using the edit button). You can refer to examples from previous Agda Implementors meetings

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.
Template 2 More complex
Presenter 2

Paragraph 1

Paragraph 2

  • Bullet 1
  • Bullet 2
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.
War Stories from the Trenches -- using Agda in Industry
Ulf Norell
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.

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

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.
(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.
Improve condition termination checking
Thorsten Altenkirch
Investigate wether we can allow hcomp and transp to be productivity preserving.
Proposal 2 with webpage
Proposer
  • Item 1
    • Subitem 1
    • Subitem 2
  • Item 2
    • Subitem 1
      • Subsubitem 1

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

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.

Organising committee

Participants

Attending in person

  • Anton Setzer, Swansea University (second homepage)
  • Monika Seisenberger, Swansea University
  • Olga Petrovska, Swansea University
  • Mukesh Tiwari, now Swansea University
  • Fahad Faleh Alhabardi, 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

Attending online

  • Arthur Scott
  • Corey Thuro

Wrap-up Notes

Note: For people reading the wrap-up notes, it is easier if they are grouped first by subject, then by date, rather than the other way around.

Monday 13 May

TODO Template

  • Item 1
  • Item 2

Tuesday 14 May

TODO Template

  • Item 1
  • Item 2

Wednesday 15 May

TODO Template

  • Item 1
  • Item 2

Thursday 16 May

TODO Template

  • Item 1
  • Item 2

Friday 17 May

TODO Template

  • Item 1
  • Item 2
Edit | History | Recent Changes (all) | Search
Page last modified on April 26, 2024, at 11:03 am
Powered by PmWiki