Andor Pénzes

Standard Chartered

I am a functional programming enthusiast in the neverending search for new technologies and solutions for creating correct software. I worked as a software engineer and test automation engineer, and now I am a Haskell developer. In recent years, Idris caught my attention, and I experimented with dependent types in general software construction.

Examples of easy dependently typed programming (in Idris)

Dependently typed programming is a green field. I want to present my experiences with Idris and how dependent types would fit into everyday programming, where proofs are not relevant but software correctness is still essential. I think dependently typed programming is not only for proof engineering.

In this talk, I will present a few approaches that don't require a deep knowledge of mathematics but solve problems around software correctness. I guarantee you will understand this talk if you know how to write algebraic data types and functions in an FP language.

OBJECTIVES

Teach the basics of everyday/industrial dependently typed programming to the audience, using simple examples written in Idris, cherry-picked from https://github.com/andorp/order-taking/ and https://github.com/andorp/IdrisExtSTGCodegen

AUDIENCE

This talk is for everyone interested in FP who knows algebraic datatypes (ADTs) and simple functions.

Slides
←Back