A gentle introduction to functional programming with dependent types.
Dependent types can enhance the 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, & type classes, and while so far mostly being used to formalize mathematics and for software verification, it is also an elegant modern powerful general-purpose programming language.

No prior knowledge of dependent types is required, but some basic understanding of functional and typed programming would be helpful.

Please install Lean4 ahead of the workshop to follow along the interactive demo and tutorial with some short exercises.
(If you use Fedora or EPEL, you can use https://copr.fedorainfracloud.org/coprs/petersen/lean4/ -- or easier, it can also be installed via the VSCode Lean4 plugin.)

https://lean-lang.org/
https://github.com/leanprover/lean4/