Idris - Dependent Types

Agenda:

• Generel intro til dependent types - hvad er de for en størrelse? - 15
  minutter

• Simple dependent types i Idris - demo / live coding - 45 minutter

-- Statisk bounds på lookup i lists

• Pause

• Universes som design pattern - 45 minutter

-- Well-typed interpreter - fortolker for simpel funktionel sprog, hvor typesystemet for Idris garanterer typekorrekthed for det fortolkede sprog

• Pause

• Idris type providers - 30 minutter

-- Demo: simpel SQLite type provider

• Hvad næste? Hvordan bliver man involveret i Idris? - 10 minutter

Om foredragsholderen (english):

David Christiansen is a third-year Ph.D. student in the Software Development Group at ITU. Currently he is working on the Actulus project. The project is a cooperation between Edlund, A/S, the Department of Mathematics at Copenhagen University and ITU. The Actulus project (short for "Actuarial calculus and computing") is a platform that includes a high level DSL to represent pension plans and life insurance models - supported by an efficient computational core.

David has extensive experience with functional programming in general and co-teaches several courses in the programming language specialization at ITU.