Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Mon 14 Jan 2019 14:00 - 15:30 at Sala V - Tutorial 5A
Mon 14 Jan 2019 16:00 - 17:30 at Sala V - Tutorial 5B

In a dependently typed programming language you can get much stronger static guarantees about the correctness of your program than in most other languages. At the same time, dependent types enable new forms of interactive programming, by letting the types guide the construction of the program. Dependently typed languages have existed for many years, but only recently have they become usable for practical programming.

In this tutorial, you will learn how to write correct-by-construction programs in the dependently typed programming language Agda. Concretely, we will together implement a verified typechecker and interpreter for a small C-like imperative language. Along the way, We will explore several modern features of the Agda language that make this task more pleasant, such as dependent pattern matching, monads and do-notation, coinduction and copattern matching, instance arguments, sized types, and the Haskell FFI.

Mon 14 Jan

POPL-2019-TutorialFest
14:00 - 15:30: TutorialFest - Tutorial 5A at Sala V
POPL-2019-TutorialFest14:00 - 15:30
Talk
Andreas AbelGothenburg University, Jesper CockxChalmers | University of Gothenburg
POPL-2019-TutorialFest
16:00 - 17:30: TutorialFest - Tutorial 5B at Sala V
POPL-2019-TutorialFest16:00 - 17:30
Talk
Andreas AbelGothenburg University, Jesper CockxChalmers | University of Gothenburg