2025-03-01 –, Shivneri Room | Chanakya Building / School of Business (capacity 200)
A gentle introduction to functional programming with dependent types.
Dependent types enhance precision and safety of programs, allowing programmers to design software with higher assurance guarantees.
Various interesting examples will be presented to illustrate the use of Dependent Type Theory, using the Lean4 programming language and theorem prover.
Lean4 has some nice features like interactive evaluation, compilation to native code, and while so far mostly being used to formalize mathematics it is also a formidable modern elegant programming language.
Intermediate - attendees should be familiar with the subject
Jens Petersen is a Engineering Manager at Red Hat working on Fedora and RHEL i18n. He is keen on Functional Programming, including Haskell.