Past Meetup

Guaranteed-Correct Programs using Dependent Types

This Meetup is past

28 people went

Details

Víctor ( https://lopezjuan.com/ ) will do an introduction to dependently typed programming, in which you can guarantee that your program is correct before even running it!

mind=blown

PugglePay/Zimpler will sponsor pizzas as usual!



I will use the Agda language for the tutorial. Everything we'll see applies to any other functional language with dependent types (e.g. Idris).

Agda is almost always used from its (impressive) interactive emacs mode. Setup instructions @ http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Download .

(and, obligatory link: https://www.youtube.com/watch?v=oKUscEWPVAM )