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