The 8th Agda Implementors' Meeting

AIM8

Gothenburg, Thursday 29 May - Wednesday 4 June, 2008

Tentative program

Roughly half of Thursday and of Friday will be talks, the rest of the time (except weekend) will be code-sprint.

PM from the planning discussion on Thursday

Thursday

place: ES52

9am
coffee
9.30
Ulf Norell, Agda news
10.30
coffee
10.45
Wouter Swiersta
11.30
Andreas Abel, "Mugda", a small dependently typed language with type-based termination.
12.15
lunch
2pm
Nils Anders Danielsson, Improved handling of mixfix operators: Design and implementation
2.45
code-sprint discussion + start of code-sprint

Friday

place: ES52

9am
Tatsuya Abe, Formalization and test generation for a CPU architecture
9.45
Ana Bove
10.30
coffee
10.45
Shunsuke Yatabe, Agda implementation of an epistemic modal logic
11.30
Andrés Sicard
12.15
lunch
2.15pm
Fredrik Lindblad (moved to Monday)
3pm
code-sprint
evening
dinner at restaurant

Saturday

evening
night out at Nefertiti

Sunday

If weather permits: excursion to Vrångö (an island in Gothenburg's archipelago).

Tram 11 from Brunnsparken at 11:45. Boat from Saltholmen to Vrångö at 12:30.

Bring your own picnic (and swim suit).

Monday

9.30
Fredrik Lindblad
after the talk
Universe Polymorphism discussion (Nils Anders Danielsson)

code-sprint

Tuesday

9.00
Coffe
9.30
Code sprint
11.00
Discussion about Type Classes (Ulf)

code-sprint

Wednesday

9.00
Coffee
9.30
Code sprint
11.00
Plugins How, which, why, when, who (Makoto)

code-sprint

15.00
Conclusion and Future directions
evening
farewell dinner at restaurant

PM from Planning Discussion on Thursday

Discussion Topics

  • Universe Polymorphism (Nisse, Monday 11.00 - 12.00)
  • Type classes (Ulf, Tuesday 11.00 - 12.00)
  • Plugins How, which, why, when, who (Makoto, Wednesday 11.00 - 1200)

Dayly meeting

  • Monday & Tuesday : 17.30 --
  • Wednesday (Conclusion and Future directions) : 15.00 --

Sprint

  • Ulf, 3: codata: add the basic productivity checker. see the feedback.
  • Yoshiki, 4: documentation?
  • Nisse, 1: fixity declarations
  • Wouter, 2:typed compiler
  • Wouter, 2:views on power lists
  • dropped: universe transformers
  • Andreas 4 :sized types in Agda implementation
  • Makoto 2: MAlonzo foreign pragmas
  • Makoto 4: Library framework for Logics
  • Patrik: case studies around Algebra of Programming (http://www.iis.sinica.edu.tw/~scm/2008/aopa/) or Generic Programming (continuation of http://portal.acm.org/citation.cfm?id=985801 )
  • Thierry 4: Finishing Mini-TT paper