Agda Implementors' Meeting XXXI

Due to the ongoing COVID-19 pandemic, AIM XXXI is postponed, to be held later this year.

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

  • Artjoms Šinkarovs: Making Sense of APL using Dependent Types.
    Multi-dimensional arrays play a major role in machine learning, numerical simulations or high-performance computing. Array programming in imperative languages involves explicit indexing within loop-nests which often leads to the code that is difficult to understand or reason about. APL offers a notation for array operations that is built around the notion of index-free combinators. APL programs are very concise yet carry very rich semantics. However, as APL is dynamically typed, reasoning about correctness of these programs is challenging.
    Designing a type system for APL is even more challenging. First, the same operator has different behavior depending on the type and shape of its arguments. Secondly, the shape of the result of an operator typically depends on the shape of its arguments. Finally, the type of array elements may change at runtime.
    In this talk I will describe preliminary results on formalising APL in Agda. I will present a shallow embedding of a core array language that makes it possible to define a set of APL operators and partially solve the overloading. As a result, a large set of APL programs can be translated into the proposed system. They can be then analysed for correctness or interpreted within Agda or compiled into executables.
    Following my talk, I will lead a discussion on rank-polymorphic multi-dimensional arrays and countable ordinals < e0, and including these in the Agda standard library.
  • Arved Friedemann: Clause Learning for Functional Solving Systems
    Since Agda and many other languages now have a reflection feature, solving systems for proof search etc. have the chance to be natively implemented into a language. There are functional style solving systems, like Schrijvers et al's Haskell Constraint Programming library, that give a good basis for logic programming in a functional language. However, there are still some optimisations needed to compete with the speed of specialised systems like in the area of SAT and SMT. One of these features is Clause Learning. The here is, that normal function application does not work anymore. The reason is, that, as soon as a conflict arises, one needs to backtrack exactly as to what caused it and add clauses stating how to fix it. As in usual functions, the origins of values are not known, they need to be wrapped in some address or bookkeeping monad. In this talk, solutions around the problem will be discussed.
  • Conor McBride: TBC
  • 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.
  • 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.
  • Uma Zalakain: Typing a linear π-calculus
    I will present the syntax, operational semantics, and typing rules of a π-calculus with linear and shared types. We use leftover typing to encode our typing rules in a way that propagates linearity constraints into process continuations. We generalize the algebras on multiplicities using partial commutative monoids, allowing the user to choose a mix of linear, affine, gradual and shared typing. We provide framing, weakening and strengthening proofs that we then use to prove subject congruence. We show that the type system is stable under substitution and prove subject reduction (aka type preservation).
  • Víctor López Juan: TBC
  • (your talk here)

Code sprint suggestions

  • Artjoms Šinkarovs: Arrays and Ordinals in the Standard Library
    I have implementations of rank-polymorphic multi-dimensional arrays, and of countable ordinals, and I would like to work on including these in the standard library.
  • Conor McBride: Contraction Pattern
  • 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`.
  • Víctor López Juan: Twin types for the Agda conversion checker
  • 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.
  • (your code sprint here)

Participants

  • Andreas Abel
  • Arjen Rouvoet
  • Artjoms Šinkarovs
  • Arved Friedemann
  • Guillaume Allais
  • Conor McBride
  • James Wood
  • John Leo
  • Orestis Melkonian
  • Swaraj Dash
  • Uma Zalakain
  • Víctor López Juan
  • Wen Kokke
  • (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:
Page last modified on May 16, 2020, at 08:39 AM
Powered by PmWiki