Agda Implementors' Meeting XXVII

The twenty-seventh Agda Implementors' Meeting will take place in Göteborg, Sweden from 2018-06-04 to 2018-06-09 (Monday to Saturday). 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

2018-05-27: Registration deadline (soft)
2018-06-04 (Mo) to 2018-06-09 (Sat): AIM XXVII

Registration

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

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

    Registration form for Agda Implementors' Meeting XXVII

    Name:

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

    Suggestions for code sprints (optional):

    Additional comments:

Note that if you want to stay at SGS Veckobostäder (see below) it may be wise to book a room as soon as possible.

Talks

Presentations on theory, implementation, and use cases of Agda and type theory are welcome.

If you would like to present something, you can propose a talk either when you register, or, write an email to Jesper.

John Leo: Musical Ornaments

Research into and practice of functional programming and dependent type theory point to a future convergence of programming and mathematics, in which one can use the machinery of mathematics to both aid in the creation of programs and to reason about them. One hurdle to progress is the problem of how to deal with a multiplicity of equivalent natural representations of data, as well as augmentation of a data structure with additional information. Automated transport of equivalences (a feature of homotopy type theory) and the theory of ornaments are techniques that have been developed to address these issues. However they have not yet seen application in practical programming.

This work in progress focuses on a toolkit written using dependent types which aims to form the basis for practical programs which synthesize and analyze music. Music is a rich yet circumscribed domain in which issues of equivalence and ornamentation naturally arise. For example a musical score can be interpreted either horizontally (counterpoint) or vertically (harmony) and it is important to be able to seamlessly convert between these representations. Similarly one may wish to treat pitch or rhythm separately as well as combine them, which is a natural application of ornamentation. We examine the extent to which this cutting-edge research can be put to use in a practical domain.

Jesper Cockx: Prop for Agda: a universe of definitionally proof-irrelevant propositions

Once upon a time, Agda had a Prop universe. Now I'm raising it back from the dead. In this talk I will motivate why you may want to use Prop, what rules it follows, and how it differs from Prop in That Other Proof Assistant.

Frederik Hanghøj Iversen: A formalization of category theory in Cubical Agda

The usual notion of propositional equality in intensional type-theory is restrictive. For instance it does not admit functional extensionality or univalence. This poses a severe limitation on both what is _provable_ and the _re-usability_ of proofs. Recent developments have, however, resulted in cubical type theory which permits a constructive proof of these two important notions. The programming language Agda has been extended with capabilities for working in such a cubical setting. This thesis will explore the usefulness of this extension in the context of category theory.

The thesis will motivate and explain why propositional equality in cubical Agda is more expressive than in standard Agda. Alternative approaches to Cubical Agda will be presented and their pros and cons will be explained. It will emphasize why it is useful to have a constructive interpretation of univalence. As an example of this two formulations of monads will be presented: Namely monaeds in the monoidal form an monads in the Kleisli form. Finally the thesis will explain the challenges that a developer will face when working with cubical Agda and give some techniques to overcome these difficulties. It will also try to suggest how future work can help alleviate some of these challenges.

Ulf Norell: The Agda Abstract Machine

Since the olden days, Agda has been using a substitution-based call-by-name evaluation strategy with all the associated problems. In this talk I will describe my efforts to bring Agda into the late 1980's: introducing the Agda Abstract Machine. The abstract machine is an environment-based call-by-need machine, solving both the substitution problem and the call-by-name issue. Some interesting challenges are introduced by the fact that we evaluate open terms, and are constrained by the existing term representation of Agda.

Andreas Abel: On formalizing lambda-definability and normalization-by-evaluation in Agda

Lambda-definability is concerned with the question: Given a (set-theoretic/mathematical) function, is there a lambda-term that implements this function? This question has been asked for untyped lambda calculus (computability) and typed lambda calculi. In the 1980s/90s Kripke models have been presented to characterize lambda-definability e.g. simply-typed lambda-calculus. It turned out that from a proof of lambda-definability one can extract a lambda-term in normal form. Thus, the computational content of lambda-definability is normalization-by-evaluation.

In this talk, I will present a formalization of lambda-definability for simple types in Agda. This is a great example to understand Kripke models and the connection between normalization and semantic completeness of the rules of intuitionistic propositional logic.

Pierre Kraft: Actors formalized in Agda (master thesis)
James Chapman: Kits for Hutton's Razor or Type Unsafe and Scope Unsafe Programs and Their Proofs

The paper Type-and-Scope Safe Programs and Their Proofs abstracts the common type-and-scope safe structure from computations on lambda-terms that deliver, e.g., renaming, substitution, evaluation, CPS-transformation, and printing with a name supply. By exposing this structure, we can prove generic simulation and fusion lemmas relating operations built this way. In this talk I will present this approach but for simpler setting of Hutton's Razor. This reduces the mathematical structures involved from relative structures to the ordinary counterparts.

Daily Schedule

Daily schedule
09.30	Session 1: Talks & Discussions
10.30	Coffee break
11.00	Session 2: Talks & Discussions
12.00	Lunch
13.15	Code sprints
15.00	Coffee break
15.30	Code sprints
17.30	Wrap-up meeting

Detailed program

Monday, 4 June
09.30	Introduction & planning
10.30	Coffee break
11.00	John Leo: Musical Ornaments
12.00	Lunch
13.15	Code sprints
15.00	Coffee break
15.30	Code sprints
17.30	Wrap-up meeting
Tuesday, 5 June
09.30	Frederik Hanghøj Iversen: A formalization of category theory in Cubical Agda
10.30	Coffee break
11.00	Jesper Cockx: Prop for Agda -- a universe of definitionally proof-irrelevant propositions
12.00	Lunch
13.15	Code sprints
15.00	Coffee break
15.30	Code sprints
17.30	Wrap-up meeting
Wednesday, 6 June
all day	Excursion to Vrångö
Thursday, 7 June
09.30	Ulf Norell: The Agda Abstract Machine
10.30	Coffee break
11.00	Andreas Abel: On formalizing lambda-definability and normalization-by-evaluation in Agda
12.00	Lunch
13.30	James Chapman: Kits for Hutton's Razor
15.00	Coffee break
16.00	(Joint session with the Initial Types Club) Pierre Kraft: Actors formalized in Agda (master thesis)
17.30	Wrap-up meeting
Friday, 8 June
09.30	Talks & Discussions
10.00	Excursion to EDIT EA to listen to Parametricity and Noninterference revisited, Maximilian Algehed
	(room EA is on the fourth floor on the eastern side of the building)
10.30	Coffee break
11.00	Planning of AIM XXVIII
12.00	Lunch
13.15	Code sprints
15.00	Coffee break
15.30	Code sprints
17.30	Wrap-up meeting
Satuday, 9 June (Different room: EDIT 8103!)
09.30	Talks & Discussions
10.30	Coffee break
11.00	Talks & Discussions
12.00	Lunch
13.15	Code sprints
15.00	Coffee break
15.30	Code sprints
17.30	Wrap-up meeting

Participants

Jesper Cockx
Nils Anders Danielsson
John Leo
Andreas Abel
Sandro Stucki
Ulf Norell
Andrea Vezzosi
James Chapman
Frederik (Folkmar) Ramcke
Jannis Limperg
Andreas Källberg
Jonathan Prieto

Suggestions for code sprints and discussions

Continue Agsy rewrite (John Leo)
Creating online repositories for teaching material, formalizations, and tools/libraries for and in Agda (Sandro Stucki)
A recurring theme of Agda meetings: experiments with cumulativity (Jesper Cockx)
Adding linearity to Agda (Andreas Abel)
Merge the 'generalize' PR and look at the code (Ulf Norell)

Location

The meeting will be in Chalmers Teknikpark, which is a few minutes walking distance from Department of Computer Science and Engineering at Chalmers University of Technology (Campus Johanneberg). Look for room Artemis. A receptionist should be sitting by the entrance, and will be able to help you find your way.

Saturday the 9th the meeting will be in the lunch room of the department.

From the central train station, you can go to Chalmers by public transportation:

Tram 7 with direction Tynnered
Tram 13 with direction Sahlgrenska via Skånegatan
Bus 58 with direction Brottkärr

You can also go to Chalmers from the transportation hub Brunnsparken, a few minutes walk from the central station:

Tram 7 with direction Tynnered
Tram 10 with direction Guldheden
Bus 16 with direction Högsbohöjd
Bus 19 with direction Fredriksdal or Bifrost (get off at Chalmers Tvärgata)
Bus 58 with direction Brottkärr

A short walk from the tram stop at Chalmers will take you to the venue Chalmers Teknikpark for the meeting.

Excursion

On June 6 (Wednesday) there will be a one-day excursion. If the weather permits, we will take the ferry to Vrångö in the Southern Göteborg Archipelago for a hike (4 km) and a barbecue on the beach.

Timetable:

10:30 Gather at Stenspiren in the city center.
10:50 Take the ferry to Vrångö.
12:25 Arrive at Vrångö
???
19:30 (or later) Take the ferry back

Bring:

a one-day Västtrafik ticket for the Göteborg area (95 kr).
comfortable shoes
water
rain gear / sun screen, depending on the weather
swimsuit & towel, if you are up for an attempt at swimming.

Travel to Göteborg

Local airport: Landvetter. There is an airport shuttle operated by Flygbussarna that takes you to the city center. You can buy tickets online at a small discount, or on board with a credit card. A ticket local transport for 90 minutes is included in the shuttle ticket. Make sure to ask the bus driver for it before you leave the bus.

Göteborg is served by trains by SJ. For information how to get here from overseas, see for instance The Man in Seat Sixty-One... and Deutsche Bahn.

Travel inside Gothenburg

All local transport inside Gothenburg is managed by Västtrafik and its subcontractors. On trams, you can buy single tickets with a credit card on board for 29kr. You cannot buy tickets onboard buses. All tickets are valid on all trams, (blue) buses and ferries inside Gothenburg for 90 minutes.

Tickets can also be purchased at 7-Eleven and Pressbyrån, or via the app (Android and iOS). If you plan to travel daily, you can buy a reloadable card for 50 kr deposit + 100 kr minimum top-up. Each trip inside the city with a reloadable card or via the app costs of 26 kr. The deposit is used to cover the cost of a trip when there is not enough money on the card. It is possible for two or more of people to travel on the same card. Ask a local to help you use the card reader.

Accommodation

You may want to use SGS Veckobostäder (350 SEK/night for a single room if you stay for 8 nights). There are many other options.

Edit | History | Recent Changes (all) | Search

Page last modified on June 08, 2018, at 07:38 am