Jesper is an assistant professor at the programming languages group at TU Delft, where he works on dependently typed languages. He is one of the core contributors to Agda.

Programming and Proving in Agda

Agda is a purely functional programming language that is similar to Haskell but has a more powerful dependent type system. With dependent types, you can express logical properties of your programs in their types and enforce them statically.

This workshop is aimed at people with at least a basic knowledge of Haskell who want to learn more about Agda and dependent types in general. By the end of this workshop, you will be able to use dependent pattern matching and equational reasoning to write formally verified programs in Agda.

[ Ссылка ]
[ Ссылка ]

свернуть