Program etc.

Wireless access

You can use eduroam or, after application by us, a guest account.

Program

Talks and discussions take place in the EDIT room (room 3364) in the building which houses the Department of Computer Science and Engineering at Chalmers University of Technology (Campus Johanneberg). Most code sprints take place in the department's lunch room.

• Wed Apr 6

  9:00-9:10	Opening of the meeting
  9:10-9:55	Andreas Abel: Higher-Order Pattern Unification for Dependently Typed Records
  9:55-10:15	Coffee break
  10:15-11:00	Dominique Devriese: Non-Canonical Implicit Arguments for Agda
  11:00-11:45	Meta-programming features; discussion leader: Nicolas Pouillard
  12:00-13:30	Lunch
  13:30-18:30	Code sprints, including coordination (in the EDIT room) CodeSprintDiscussion
• Thu Apr 7

  9:00-9:45	Olle Fredriksson & Daniel Gustafsson: Making an Epic backend for Agda
  9:45-10:15	Coffee break
  10:15-11:00	Simon Foster: Experiences with integrating an automated theorem prover into Agda
  11:00-11:45	Karim Kanso: Light-Weight Approach to Integrate Agda with Automated Theorem Provers
  12:00-13:30	Lunch
  13:30-18:30	Code sprints
• Fri Apr 8

  9:00-9:45	Ana Bove & Peter Dybjer: Combining Automatic and Interactive Proof in First Order Theories of Combinators
  9:45-10:15	Coffee break
  10:15-11:00	Thorsten Altenkirch and/or Thierry Coquand: Discussion about homotopy type theory
  11:00-12:00	Code sprints
  12:00-13:30	Lunch
  13:30-18:00	Code sprints
  19:00-	Dinner, Sukhothai
• Sat Apr 9
  We plan to go for a walk in Vättlefjäll. You may want to bring good shoes or boots for walking, and something to protect you in case of sudden bad weather.
  We will stop and have lunch next to a lake. As far as we know it is not possible to buy food in the forest, so we suggest that you bring some food with you.
  You can take a bus back from the walk, but you cannot buy bus tickets on the bus. The easiest solution for you may be to buy a one-day travel card before leaving for the walk. These are for instance sold in one or more kiosks around campus (these kiosks may or may not be open on Saturday morning). More information about tickets.
  Route for the walk: Mölnesjön, Grästjärnet, Stentjärna, Skyrsjön, Andtjärn, Gäddevattnet, Surtesjön, Skrovtjärn, Toleredssjön, Vättlestugan (roughly 12 km).
  We start from Fjällbruden (a bus stop) at 10:55, and return from the bus stop Kryddnejlikegatan. At least one of us will leave from the Chalmers tram stop at 10:03 (tram 10 to Brunnsparken, then tram 9 at 10:21 to Angered, and finally bus 76 at 10:45 to Fjällbruden). One possible option for the return trip is to take bus 75 from Kryddnejlikegatan at 14:37 and tram 8 from Angered at 14:54, arriving at Chalmers at 15:23. You can consult Västtrafik's travel planner for more options.
• Sun Apr 10
  We plan to go to Gunnebo Slott och Trädgårdar. The castle has very nice gardens, a café and a farm.
  The idea is to get the guided tour to the castle at 1pm (entrance fee 80 sek).
  On Sunday there is also a piano jazz concert at 3pm by Lars Jansson (entrance fee 100 sek),
  To make it to the guided tour we can take bus number 753 to Kristinedal. Here is the time table of the bus in the direction to the castle.
  From Chalmers main entrance we need to take the bus at 11.30. From there it takes about 35 minutes to Kristinedal, and then we need to walk ca 15 min.
  Remember that you cannot buy tickets on the bus. When buying the tickets in a shop (see how to buy tickets on the excursion on Saturday) you must say that you need tickets to and from Gunnebo Slott. The castle is located outside Gothenburg so if you simply buy a ticket valid within the city you will not be able to use it to go to the castle.
• Mon Apr 11

  9:00-9:45	Anton Setzer: Extraction of programs from proofs using postulated axioms (slides, Agda code)
  9:45-10:15	Coffee break
  10:15-12:00	Code sprints
  12:00-13:30	Lunch
  13:30-18:30	Code sprints
• Tue Apr 12

  9:00-9:45	Wolfram Kahl: Using Agda for Formalisation of Typed Term Graphs and of Relation-Algebraic Categories
  9:45-10:15	Coffee break
  10:15-12:00	Code sprints
  12:00-13:30	Lunch
  13:30-14:00	Code sprints (in the EDIT room)
  14:00-17:00	Code sprint debriefing (in the EDIT room)

  AIMXIV

Abstracts

• Dominique Devriese: Non-Canonical Implicit Arguments for Agda
  We propose non-canonical implicit arguments: a new feature for Agda and an alternative to Haskell type classes. We do not encode type classes directly, but provide a simpler, more elegant and more general feature, inspired upon Scala implicits and Agda implicit arguments. Our instance search is unambiguous, non-recursive and predictable. In this presentation, we will present the proposed feature with some technical details and live demo's of example code using our Agda implementation.
• Simon Foster: Experiences with integrating an automated theorem prover into Agda
  I have recently completed an integration of the equational reasoner Waldmeister into Agda. Such integrations could greatly improve the automation of simple proof tasks in Agda and liberate users to focus on the more interesting aspects of proofs. This integration allows equational proofs of propositional equality to be automatically derived from suitable assumptions. The equality goal to be proved is restated using a sound reflection layer and passed to Waldmeister. Its proof output can then be reconstructed by a supplied Agda function, yielding a propositional equality proof. Currently there is still scope for improving the integration from the user side and proof reconstruction is often inefficient. In this talk I will outline how the integration works and hopefully provide a discussion point for how such integrations could be improved and made more generic in the future.
• Olle Fredriksson & Daniel Gustafsson: Making an Epic backend for Agda
  During our master's thesis we have created a new compiler backend for Agda, compiling to Epic, and implemented some optimisations. We will talk about some optimisations that are done in the backend, including forcing, primitive datatypes, partial evaluation and injection detection. We also hope to show some actual Agda programs running.
• Wolfram Kahl: Using Agda for Formalisation of Typed Term Graphs and of Relation-Algebraic Categories
  My ongoing projects with Agda also happen to sit on two sides of an important current limitation of Agda: My theories of relation-algebraic categories are “unreasonably” ressource-hungry, apparently due to lack of sharing in the implementation of Agda, and term graphs formalisms are where such sharing is studied in general.
• Anton Setzer: Extraction of programs from proofs using postulated axioms (joint work with Chi Ming Chuang, Swansea)
  We give a axiomatisation of a theory of real numbers which includes the set of real numbers which are approximable by signed digit representation. The latter set is given as a coalgebraic type. We define a trivial function which extracts programs from proofs using this axiomatisations. Since the axiomatisation is based on postulate it is not clear whether this extraction function computes values in head normal form. We state conditions under which this is the case and show that under these conditions values in head normal form are computed. This makes use of a reduction of nested pattern matching by simple pattern matching.