Main /
\ Main

AIMXIX

The nineteenth edition of the Agda Implementors' Meeting: Theory, implementation, and applications of Agda.

The nineteenth Agda Implementors' Meeting will be held in Paris 22-28 May 2014 (Thu to Wed). Everyone with a genuine interest in Agda is invited to attend. 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.

As a special opportunity, due to the location, we hope for the attendence of the Coq developers and strongly encourage: 

  * Presentations on the design and implementation of languages for
    Type Theory in general.

  * Exchange of ideas between Coq and Agda developers.

Venue

AIM XIX takes place 22-28 May 2014 in Paris, in conjunction with the IHP trimester on proofs.

The location is the Institute Henri Pointcare, 11, rue Pierre et Marie Curie Paris 75005, in the following rooms:

Thu314
Fr morning421
Fr afternoonAmphiteater Perrin first left in building opposite of IHP
Mon - Wed201

Amphitheater Perrin is at the Institut de Chimie Physique just opposite of the entry to IHP .

Wireless: IHP1234

Printing: Use network printers (upload .ps or .pdf)

2nd floorljet2.ihp.fr
3rd floorljet3.ihp.fr
4th floorljet4.ihp.fr

Daily Schedule

9.30Gather. Coffee (50c) machine in ground floor, tea kitchen in 2nd floor
10.00Talks, discussions, code sprints
12.00Lunch break
13.30Discussions and code sprints
18.00Wrap up (progress reports)

Lunch options:

  • Quick: Sandwiches from Boulangeries; Creperies; etc around the campus
  • Full: Cantine in the Ecole Normale Superieure, 45 Rue d'Ulm. Ask for directions at the entry. Tickets are 9 EUR, sold only until 13.30. Better be there around 13.00.
  • Restaurants on Rue Mouffetard.

Dinner options:

  • Rue Mouffetard is close by and has a great variety of affordable restaurants.

Program

(not etched in stone)

Thu 22ndRoom 314
10.00Jesper Cockx, Eliminating dependent pattern matching without K
10.45Introduction of participants; code sprint proposals
14.00Andreas Abel, Introduction to Agda's internals and live bug fixing session
18.00Wrap-up meeting
Fri 23ndRoom 421
10.00Nicolas Pouillard, Dependent Protocols for Communication
afternoonAmphiteater Perrin
14.00Ambrus Kaposi, A Syntax for Cubical Type Theory (slides at http://mazzo.li/dump/aim-kaposi-pres.pdf )
18.00Wrap-up meeting
Mon 26thRoom 201
10.00Sergei Sinchuk, Coq-verified operational transformation for trees
11.00Christoph Senjak, Verfying Deflate Trees (Unzip)
18.00Wrap-up meeting
Tue 27thRoom 201
10.00Matthieu Sozeau, Universe polymorphism in Coq
18.00Wrap-up meeting
Wed 28thRoom 421
10.00Happy hacking!
18.00Wrap-up meeting

Note: Thu 29th May after the meeting is a public holiday in France (ascension).

Excursion Sat 24th May

Excursion to Fontainebleau (south of Paris). Guilhem, Ambrus, Jesper (with Anders Mortberg). 

  10.00 Meet at Gare d'Lyon
  10.19 Train Gare d'Lyon - Melon (Banlieue 151821, directon Montargis)
  11.00 Arive at Fontainebleau-Avon

Alternative (with train, then bus from Melon) 

  10.45 arrive at Melon
  11.20 Bus from Place de L'Erimtage (direction Place Verdun)
  11.40 arrive at Chateau Fontainebleau

Alternative Excursion: Louvre (meet 10 am at Pyramid). James, Andrea, Christoph, Andreas.

Talks

Jesper Cockx, Eliminating dependent pattern matching without K

Dependent pattern matching is a fundamental technique for writing Agda code, but by default it implies the K axiom, making it incompatible with homotopy type theory. The --without-K flag imposes a syntactic check for definitions that rely on K, however so far it lacked a formal correctness proof. In this talk, I propose a new specification for --without-K that works by limiting the unification algorithm used for case splitting. It is strictly more liberal than the current specification, particularly when pattern matching on parametrized datatypes, and at the same time it solves a currently open problem with the syntactic check. More importantly, it allows a translation of definitions by pattern matching to eliminators in the style of Goguen et al. (2006) without relying on the K axiom, thus proving its correctness. So with it, we can finally stop worrying when using pattern matching in HoTT.

Sergei Sinchuk, Coq-verified operational transformation for trees.

Operational transformation (OT) is an approach to concurrency control and consistency maintenance in collaborative applications proposed by C. Ellis and S. Gibbs in 1989. Google Wave and Google Docs serve as better-known implementations of this approach. The problem of designing an OT algorithm is known to be a hard and error-prone task even for the simplest types of shared data (e.g. plain text). As illustrated in a recent work by A. Imine, A. Randolph et al. the majority of implementations of OT published in the literature contain mistakes and do not possess the claimed consistency properties. In my talk I am going to share experience gained from the recent successful development of a complex OT algorithm for collaborative editing of XML-like structured data whose correctness has been verified by means of Coq proof assistant.

Nicolas Pouillard, Dependent Protocols for Communication

Programming correct and precise communicating systems remains a challenging and error-prone venture. Still, communicating systems are not only used in practice everyday but also as a device for game based proofs such as security notions. We present a shallow embedding of protocols within the dependent type theory of Agda, enabling mechanized formal reasoning of processes following precise protocols. Using this shallow embedding we reconstruct the connectives from linear logic, and provide an elegant reasoning tool for communicating systems, all within a purely functional dependently typed programming language.

Ambrus Kaposi, A syntax for cubical type theory

Abstract: we propose a type theory where equality is defined recursively for each type former instead of the usual inductive type with the J eliminator. By defining equality for the universe as equivalence we get a computational understanding of the univalence axiom and also functional extensionality. This is ongoing work with Thorsten Altenkirch and is based on Bernardy and Moulin's internal parametricity and Coquand, Bezem, Huber's cubical set model.

Christoph-Simon Senjak, Formally Verifying Deflate-Trees (Unzip)

More talks TBA

Discussion on AIM XX dates (colocated with ICFP)

  • Alt 1: before ICFP: Mon Aug 25 - Fri Aug 29
    • Pro: before Estonian term starts (James)
    • Contra: vacation season !?, beginning of Chalmers term
    • Votes: Guillaume,
  • Alt 2: during ICFP workshops: Thu Sep 4 - Wed Sep 10
    • Pro: less time away for parents
    • Contra: Haskell Symposium is too a big competition
    • Votes: Nicolas
  • Alt 3: after ICFP: Mon Sep 8 - Fr Sep 12
    • Pro: no conflicts
    • Contra: long overall duration (ICFP + AIM), exhaustion!?
    • Votes: James, Andreas

Discussions and Code Sprint Suggestions

  • NP: Towards Higher Inductive Types in Agda
  • NP: Exposing the .. modality
  • GM: Type Theory in Colors

Nicolas Pouillard, Support for Higher Inductive Types

  • per definition PRAGMAs to enable/disable checks
    • like without-K on functions
    • on datatypes: admit K, injectivity, positivity...
  • see Guillaume's proposal of HITs
  • Jesper Cockx, Detect types that admit K
  • Favonia, Pierre-Evariste, Andreas
    • Progress:
      • Thu: Nicolas: investigating pragmas/parsing/syntax, refactored to incorporate WithK
      • Tue: dealing with Syntax infrastructure, want: turning of injectivity for constructors (for HITs)
      • Wed: demo: HIT instead of data disables no-confusion, injectivity, and no-cycle

Nicolas Pouillard, Improve Meta Programming

  • Pierre-Evariste Dagand, Andrea Vezzosi: inject definitions into Agda
  • Jesper Cockx, Francesco Mazzoli
    • Progress:
      • Wed: Jesper and Pierre discussed injecting case trees into Agda (but it is hard).

Francesco Mazzoli, Prototypical Implementation of a small TT (performance tuning)

  • Andreas Vezzosi: Unification for the prototype
  • Nicolas Pouillard, Pierre-Evariste, Andreas
    • Progress
      • Thu: found bug in prototype, changed handling of data constructors
      • Fri: found bug in Agda's unification, advanced prototypical type checker (more cases)
      • Mon: Implementing pruning
      • Tue: pruning works. Found bug in Agda's pruning (again).
      • Wed: refactoring code. More conservative pruning, probably right notion of rigid variable found.

Guilhem Moulin, Type Theory in Color

  • Nicolas, (Andreas)
    • Progress:
      • Mon: get back to old patches, try to compile them again (lots of merging needed)
      • Tue: discovered grey area in connection with inductive types. Erasure of data types does not work yet, figuring stuff out on paper.
      • Wed: discovered problem in the prototype. Pierre suggested different approach to relate Natural numbers and Lists by erasure (using the forgetful functor). More work when defining data types, but in functions the correct instance will be inferred (by color).

Guillaume Brunerie, Recursive Instance Search

  • David Darais
  • Andreas: Intro
    • Progress:
      • Fri: added instance keyword, parses, translates to abstract syntax
      • Mon: search restricts to instances; in progress: making it recursive (w/o concern about termination)
      • Wed: recursive search seems to work (successful demo)! Needs some testing yet. New feature: instance search succeeds also at function types (inserting lambdas).

Jesper, Discussion: Overlapping and Order-Independent Patterns

  • James, Andreas
  • Order-Independence: all equations hold definitionally
  • Stage 2: Overlapping patterns?? (not conservative)
    • Progress:
      • Thu: Jesper, Pierre: implementing compilation of pattern matching in Agda in a data type generic way (started)
      • Fri: Error in coverage checker when not all clauses hold definitionally, adding PRAGMA when clauses should hold definitionally
      • Mon: PRAGMA parsed and distributed into Nice syntax; next: Abstract
      • Tue: Distribution of PRAGMA to Abstract finished, but does not work
      • Wed: PRAGMA EXACT_SPLIT works, discovers clauses that do not hold definitionally! Polishing needed. Maybe have option that turns on EXACT_SPLIT for all clauses, plus pragma that turns it of for individual clauses.

James Chapman, Quotients via postulate (add to Std-Lib)

  • Progress:
    • Wed: James presented Hofmann's quotients as addition to Std-Lib

James Chapman, Negative Integer Literals

  • BUILTIN for Integers and Fin
  • Quotiented Pair or Coproduct?
    • Progress:
      • Fri: -1 is a natural number
      • Mon: looking at overloading literals (resolve during type-checking)
      • Tue: -1 + -1 = neg (suc 0)
      • Wed: something works for BUILTIN INTEGER (demo). Bugs remain.

James Chapman, NBE for Streams

  • Andreas, Andrea, Peter
    • Progress:
      • Thu: James: preparing NBE for Streams to demonstrate

James Chapman, Copatterns

  • Francesco, Andreas, Stephan
  • with
  • split on result
  • compilation

James Chapman, Worries/Discussion: Compilation

  • Agda to Idris-internal?
  • Agda to Haskell-core?

James Chapman, Windows-Installer

Andres Mörtberg, Cubical Agda

  • Andreas: Intro
  • Favonia
    • Progress:
      • Thu: discussed where to plug in Cubical into Agda

Favonia, API for Agda Server

  • Agda Server with nicer syntax
  • Interaction tests within Haskell
  • Haskell-API
  • TODO: Clean up TCState and TCEnv and make TCM closer to a nice API
    • Progress
      • Fri: read the code.
      • Mon: read more code. removed one redundant field.
      • Tue: read even more code. moved one field out of TCState. Needs more manpower.
      • Wed: Discussed splitting TCM into separate monads for scope checking, type checking, interaction. Untangle phases. Moving InteractionPoints out of the TypeChecker (work in progress).

Favonia, Guillaume: layout keywords on the same line (private, abstract...)

  • Progress
    • Thu: started
    • Fri: gave up, it's complicated. Filed as issue 1145. Need clear specification.

Andreas Abel, Release Task Force

  • Fixing bugs
    • Progress:
      • Thu: found 3 bugs, fixed one, reported one
      • Mon: Andrea, Andreas: fix issue 1147 (incorrect pruning)
  • Automate release process: Guilhem
    • Progress:
      • Thu: halfway through
      • Fri: pretty much done
  • Agda test manager: Favonia
    • HUnit: Anders

Agda on GitHub

  • Workflow: branches etc.
  • Make a transition plan: What happens with forks etc.
  • Francesco, Nicolas, Andreas

Andreas Abel, Termination Checking compatible with Univalence

  • Jesper, Pierre, Favonia
    • Progress
      • Mon: Jesper polished previous fix (could be used temporarily --without-K)

Andreas, Jesper, Adding Rewriting to Agda

  • Make the following work: 

addZ : ∀ x → x + 0 ≡ x
addZ zero    = refl
addZ (suc x) = cong suc (addZ x)

{-# BUILTIN REWRITE _≡_ #-}
{-# REWRITE addZ        #-}

addZ' : ∀ x → x + 0 ≡ x
addZ' x = refl
  • Progress:
    • Tue: Parse pragmas, check types of rewrite relation and rules. No rewriting yet.

Ali Assaf: Translation from Agda to Dedukti

  • Progress
    • Thu: looking for entry point for translation
    • Fri: Added flag to compile to deducti (does nothing yet). Ali had to leave

Christoph: Deflate trees in Coq

  • Progress
    • Fri: uniqueness proved, but not existence
    • Mon: gave talk; at last recursive step for existence
    • Tue: in the middle of a proof that Kraft inequality implies existence of a further code

Christian Sattler: Code generator for omega-categorical definitions

  • up to a certain level
  • e.g. simplicial types, algebraic definitions
  • just an idea
    • Progress:
      • Fri: initial investigations
  • reducing parametric W-types to plain W-types
  • would like to have extension of Miller pattern unification to neutrals F (x y) = t(x y) solved by F z = t(z).
    • Tue: parametric W-types continued

Ambrus Cubical type theory

  • Progress:
    • Mon: Ambrus: discussed swap operation with Andrew Polonsky
    • Tue: two dimensional swap on paper, type-checking in Latex

Participants

  • Andreas Abel
  • Stephan Adelsberger
  • Guillaume Brunerie
  • James Chapman
  • Jesper Cockx
  • Pierre-Evariste Dagand
  • Peter Dybjer
  • Favonia
  • Ambrus Kaposi
  • Hugo Macedo
  • Francesco Mazzoli
  • Guilhem Moulin
  • Anders Mörtberg
  • Nicolas Pouillard
  • Christian Sattler
  • Christoph-Simon Senjak
  • Sergei Sinchuk
  • Andrea Vezzosi

Excursion

TBA

Registration

The (soft) deadline for registration is 1st May 2014.

To register, please send an email to me (andreas dot abel at gu dot se), filling out the following form: 

Name       :
Affiliation:
email      :

Duration of participation at AIM XIX:
* Date of arrival  :
* Date of departure:

Program:
* I'd like to give a talk or lead a discussion (yes/no):
Title   :
Abstract: (optional)

* Suggestion for code-sprint (optional):
Edit | History | Recent Changes (all) | Search
Page last modified on May 28, 2014, at 05:49 pm
Powered by PmWiki