DevConf.IN 2025

Fun Programming with Dependent Types
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.


What level of experience should the audience have to best understand your session?

Intermediate - attendees should be familiar with the subject

See also:

Jens Petersen is a Engineering Manager at Red Hat working on Fedora and RHEL i18n. He is keen on Functional Programming, including Haskell.