AIMXXPlanning

 
 |--------+------------------------------------------------------------+--------|
 | Thu 16 |                                                            |        |
 |  09.00 | Orientation / Waiting                                      | JCh    |
 |  09.30 | Planning                                                   |        |
 |  10.15 | Talk: Agda’s style guide to Haskell programming 1          | AA     |
 |  10.45 | Coffee                                                     |        |
 |  11.15 | Talk: ASGHP 2, Bug fixing sample session                   | AA     |
 |  12.30 | Lunch (provided)                                           |        |
 |  14.00 | Talk: Bug fixing sample session demo                       | AA     |
 |  14.30 | Code Sprint starts                                         |        |
 |  15.30 | Coffee                                                     |        |
 |  16.00 | Code Sprint                                                |        |
 |  17.15 | Daily wrap up                                              |        |
 |        | (new unquoteDef, unquoteDecl demo)                         | UN     |
 |        | (today's progress)                                         | FM     |
 |        | (realisability for Internal TT)                            | AA, NK |
 |        | (Feferman's XXX?; instance args, exponential to quadratic) | GM     |
 |  18.00 | Finish                                                     |        |
 |--------+------------------------------------------------------------+--------|
 | Fri 17 |                                                            |        |
 |  09.00 | Hacking                                                    |        |
 |  09.30 | Talk: What's new in Agda (Recursive instance search,       | UN     |
 |        | "tactics" keyword for reflection, tactics auto,DerivingEq, |        |
 |        | Tactics.Deriving.Eq, fast well-founded rec)                |        |
 |  10.30 | Coffee                                                     |        |
 |  12.30 | Lunch (provided)                                           |        |
 |  14.00 | Talk: A realizability model for Type Theory                | KN     |
 |  14.40 | Hacking                                                    |        |
 |  15.30 | Coffee                                                     |        |
 |  17.20 | Daily wrap up                                              |        |
 |        | - UN: relaxing data type size constraint by disregarding   |        |
 |        | forced constructor args                                    |        |
 |        | - NP: Better reflection API to attach names to things,     |        |
 |        | with the exmaple of readable derived decidable eq.         |        |
 |        | - FM: Building Agda on Travis CI Service                   |        |
 |  18.00 | Finish                                                     |        |
 |--------+------------------------------------------------------------+--------|
 | Sat 18 |                                                            |        |
 |  09.00 | Hacking                                                    |        |
 |  09.30 | Talk: Type checking in the presense of meta-variabalbe     | FM     |
 |  10.30 | Coffee                                                     |        |
 |  12.30 | Lunch (provided)                                           |        |
 |  14.00 | Hacking                                                    |        |
 |  15.30 | Coffee                                                     |        |
 |  17.40 | Daily wrapup                                               |        |
 |        | - quoteContext                                             |        |
 |        | - AV: Reflection reification with names                    |        |
 |        | - AA,MT: Hunting for fat fish in Serialise.hs              |        |
 |        | - UN: Reviving mutable shared term structure               |        |
 |  18.00 | Finish                                                     |        |
 |--------+------------------------------------------------------------+--------|
 | Mon 20 |                                                            |        |
 |  09.00 | Hacking                                                    |        |
 |  10.30 | Coffee                                                     |        |
 |  12.30 | Lunch (provided)                                           |        |
 |  15.30 | Coffee                                                     |        |
 |  18.00 | Finish                                                     |        |
 | Tue 21 |                                                            |        |
 |  09.00 | Hacking                                                    |        |
 |  10.30 | Coffee                                                     |        |
 |  12.30 | Lunch (provided)                                           |        |
 |  15.30 | Coffee                                                     |        |
 |  18.00 | Finish                                                     |        |
 | Wed 22 |                                                            |        |
 |  09.00 | Hacking                                                    |        |
 |  10.30 | Coffee                                                     |        |
 |  12.30 | Lunch (provided)                                           |        |
 |  15.30 | Coffee                                                     |        |
 |  16.00 | Finish (to allow people to catch flights)                  |        |
 |        | Excursion (probably on Sunday)                             |        |

• Orientation
  - 3 rooms, armchairs
  - Thr-Sat, Mon-Tue Dayly sched

    - Starts at 9.00
    - Coffee 10.30
    - Lunch 12.30
    - Afternoot starts 14.00
    - Coffee 15.30
    - Finish at 18.00

- Sunday Free. Excursion? XXX Park, Museum, Go outside City, ..

  - Finishing early in Wed.
  - Wifi
    - ssid: SAAL or SAAL2
    - pass: saal2014
  - Beware of pickpockets, rip-off taxis
  - Sunset 18:10; Nice to have a walk around here before then.

• Talks planning - AA: Thr (Intro to src, Bug fixing example) - UN: Fri - FM: Sat? : Type checking with metavariables, unification - NV: Mon : Quotients - GB: Tue : Homotopic type theory - KN: Formalising the realisability model for Type Theory. - DF:
• CodeSprint / Self Intro

- JCh:

  - Overloaded Int literals
  - Category theory library
  - Definition of Quotients in Std lib
  - Relative Monad in Std lib.

- KN:

  - Formalising realisability model for TT, based on beta-eta red.
  - Translating paper proof with naive set theory to ...

- NV:

  - Fomalisation of math. Cat Thy, Partial Cat,
  - Partiality Monad in std lib(to work with copatterns)
  - Quotient data types, 
  - Definition of Quotients in Std lib

- SC: Formalising Group thy in Agda - AA:

  - Rewriting in Agda for HTT
  - Record proj. overloading
  - Infra to run Agda with TRAVIS
  - Developer Wiki
  - Answering All Question about Agda Source Code.

- UN:

  - Reflection. Building a whole declaration, mutual ones, ...
  - Answering All Question about Agda Source Code.

- DF:

  - Language theory. Safe evaluation of attr gr.
  - Latex backend.  (w/ Wolfgang?)

- GM:

  - w. JPB, Implementing Type Theory in Colors. 

- MT:

  - Framework to assure good properties of certain (software) process.

- FM:

  - TOG: Prototypical Impl of Agda to make it nicer, modular, ...

- AV:

  - Make Agda to skip type checking when decls are not changed.

- MA:

  - Multiple patterns (for left hand sides)?
  - Currying before termination checking?
  - Forcing and levels

- JCo

  - Rewriteing rules
  - Reflection: unquoting, local vars, ...

- GB

  - Recursive instance search algo.
  - applying it to Homotopy TT Library

- JCh, MT

  - Instruction for manually installing the latest Agda on Windows.
  - Binary distibution of Agda (on Windows). git something.