Agda Implementors' Meeting XXXI

The thirty-first Agda Implementors' Meeting will take place in Edinburgh from 2020-04-01 to 2020-04-07 (Wednesday to Tuesday). The meeting will be similar to previous ones:

  • Presentations concerning theory, implementation, and use cases of Agda.
  • Discussions around issues of the Agda language.
  • Plenty of time to work on or in Agda, in collaboration with the other participants.

Important dates

2020-03-18
Registration deadline (soft)
2020-04-01 (Wed) to 2020-04-07 (Tue)
AIM XXXI

Programme

All talks, coffee breaks and sprints take place rooms 5.02 of the Bayes Centre, University of Edinburgh.

Wednesday, 1 April
09:30Talk: TBA
10:30Coffee break
11:00Introduction: code sprint proposals, planning
12:00Lunch
13:00Groups/Code sprints/Discussions
15:00Coffee break
16:00Groups/Code sprints/Discussions
17:00Wrap-up meeting (summary)
Thursday, 2 April
09:30Talk: TBA
10:30Coffee break
11:00Groups/Code sprints/Discussions
12:00Lunch
13:00Groups/Code sprints/Discussions
15:00Coffee break
16:00Groups/Code sprints/Discussions
17:00Wrap-up meeting (summary)
Friday, 3 April
09:30Talk: TBA
10:30Coffee break
11:00Groups/Code sprints/Discussions
12:00Lunch
13:00Groups/Code sprints/Discussions
15:00Coffee break
16:00Groups/Code sprints/Discussions
17:00Wrap-up meeting (summary)
Saturday, 4 April
09:30Talk: TBA
10:30Coffee break
11:00Groups/Code sprints/Discussions
12:00Lunch
13:00Groups/Code sprints/Discussions
15:00Coffee break
16:00Groups/Code sprints/Discussions
17:00Wrap-up meeting (summary)
Sunday, 5 April
09:30Talk: TBA
10:30Coffee break
11:00Groups/Code sprints/Discussions
12:00Lunch
13:00Groups/Code sprints/Discussions
15:00Coffee break
16:00Groups/Code sprints/Discussions
17:00Wrap-up meeting (summary)
Monday, 6 April
09:30Talk: TBA
10:30Coffee break
11:00Groups/Code sprints/Discussions
12:00Lunch
13:00Groups/Code sprints/Discussions
15:00Coffee break
16:00Groups/Code sprints/Discussions
17:00Wrap-up meeting (summary)
Tuesday, 7 April
09:30Talk: TBA
10:30Coffee break
11:00Groups/Code sprints/Discussions
12:00Lunch
13:00Groups/Code sprints/Discussions
15:00Coffee break
16:00Groups/Code sprints/Discussions
17:00Wrap-up meeting (summary)

Talks

  • John Leo: Music Tools
    An update on the progress of tools written in Agda for the analysis and synthesis of music. Joint work with Youyou Cong.
  • Arjen Rouvoet: TBA
  • James Wood: Linear Algebra as Slickly as Possible
    Either: I give an overview of a bunch of tricks that make definitional equality work in my favour, or I explore correct-by-construction linear algebra.
  • Conor McBride: TBA
  • (your talk here)

Code sprint suggestions

  • Wen Kokke: Integration with SAT and SMT solvers
    For their Ph.D., Karim Kanso wrote a quite general framework for integrating Agda with SAT and SMT solvers. It would be a shame to let this code bitrot away, especially when integration with SMT solvers is such a useful tool! I propose that we asses how much effort a merge of this code into the master branch would be. (Help wanted.)
  • Guillaume Allais: Computation on the LHS
    Allowing arbitrary computations on the LHS as long as they yield a valid pattern. The first step is to do it for closed terms (which would allow us to finally bring support for literals on the LHS) but in general we may want to have open terms too! For instance, it is a lot easier to write `toList "hello " ++ xs` than `'h' ∷ 'e' ∷ 'l' ∷ 'l' ∷ 'o' ∷ ' ' ∷ xs`.
  • Conor McBride: Contraction Pattern
    TBA.
  • (your code sprint here)

Participants

  • Wen Kokke
  • Orestis Melkonian
  • John Leo
  • Swaraj Dash
  • Guillaume Allais
  • Andreas Abel
  • Arjen Rouvoet
  • James Wood
  • Conor McBride
  • (your name here)

Location

The meeting will take place in Room 5.02 of the ICMS:

Bayes Centre, The University of Edinburgh
47 Potterrow
Edinburgh EH8 9BT
Scotland

The ICMS is located at the top floor of the Bayes Centre. You can enter the building via the main doors. The building is access controlled, so you will have to sign in at the reception. Take the elevator to the fifth floor, and the ICMS will be to your right. For more detailed information, see the ICMS website.

Excursion

There will be a day-long hike on Sunday, 5 April. We will walk the 9th stage of the famous John Muir Way.
The route starts from the small village of Prestonpans and ends on the beautiful seaside town of North Berwick,
spanning a total of 25km/15.5miles and taking approximately 6-7.5 hours (check the map).

A rough estimate of the timeplan follows (subject to ad-hoc changes):

8amMeet at the University
9amArrive at Prestonpans (by train or bus)
9am-1pmFirst half of the hike
1pmLunch at Aberlady or Gullane (depending on group's pace)
1-5pmSecond half of the hike
5pmArrive at North Berwick
5-7pmCoffee/dinner and see the town
7pmTake return bus
9pmBack in Edinburgh

For any information/comments/questions/concerns (e.g. dietary restrictions), contact Orestis Melkonian.

More information will appear here.

About Edinburgh

Edinburgh is Scotland's compact, hilly capital. It has a medieval Old Town and elegant Georgian New Town with gardens and neoclassical buildings. Looming over the city is Edinburgh Castle, home to Scotlandís crown jewels and the Stone of Destiny, used in the coronation of Scottish rulers. Arthurís Seat is an imposing peak in Holyrood Park with sweeping views, and Calton Hill is topped with monuments and memorials.

More information will appear here.

Accommodation

The ICMS offers a number of suggestions for hotels nearby:

  • Edinburgh First
    Edinburgh First is the accommodation service of the University of Edinburgh and they offer good quality, well priced rooms at a number of locations in the City year round. If you book your accomodation via Edinburgh First, you can use the discount code 'EVENT' to receive a 15% discount.
  • IBIS South Bridge
    This IBIS hotel is located five-minutes walk from ICMS. There is another IBIS at Hunter Square which is a little further away towards the city centre.
  • 10 Hill Place
    This hotel is located two minutes from ICMS.
  • Jury's Inn
    Jury's Inn is a ten-minute walk from ICMS and benefits from being very close to the railway station and the airport bus bus stop.
  • Leonardo Boutique Hotel Edinburgh City
    This hotel is located on Lauriston Place and is a ten-minute walk from ICMS.
  • Premier Inn
    This chain has a number of hotels close to ICMS, including Princes Street, East Market Street and Lauriston Place.
  • Princes St Backpackers
    If you require budget accomodation, Princes St Backpackers is one of the most affordable hostels, and is about 20 minutes walk from the ICMS.
    (Note: This location was added by the organisers, and isn't recommended by the ICMS.)

Registration

You can register for the meeting by filling out the form below and emailing it to Wen Kokke.

There is no registration fee. Coffee breaks would be included. Transportation, accommodation and meals are to be covered by the participant.

    Registration form for Agda Implementors' Meeting XXXI

    Name:

    Title and optionally abstract (if you want to give a talk or lead a discussion):

    Suggestions for code sprints (optional):

    Additional comments: