Haskell Utrecht Meetup

Mark your calendars: the next Haskell Utrecht Meetup will be on February 2nd.

We will be back in the University Library - room 0.21 - in the City Center. Note that you can park your bicycle under the library if you enter through the central courtyard.

We hope to see you there! We have two speakers confirmed, Jaro Reinders and Niek Mulleners.

Agenda:

• 19:15 Doors open
• 19:30 Welcome
• 19:35 Jaro Reinders - Algebraic Effects for Verified Compilers
• Break
• 20:30 Niek Mulleners - Programming with Holes, Types, and Tests
• 21:00-ish Finish
• Drinks @ Florin

Algebraic Effects for Verified Compilers - Jaro Reijnders

Algebraic effects are a promising approach to reason about programs with side effects. Recent work on interaction trees has shown that algebraic effects can be used to verify compilers extrinsically. In the hope of avoiding overhead of extrinsic verification, I have researched how to use algebraic effects more directly as the intermediate representation in a verified compiler. I will present this approach and its complications.

Programming with Holes, Types, and Tests - Niek Mulleners

The duty of the compiler is to turn programs into executable code.
When a program is incomplete or incorrect, it should tell the programmer exactly why their program cannot be executed and, ideally, how this can be fixed. To do so, the compiler has to understand the programmer's intentions. In this talk, I will explore how programmers can express their intentions through types, tests, and sketches (programs containing holes), and how the compiler might use this information to assist them in writing programs.