Recording of My Talk at Lambda Days 2019

In February I was at the Lambda Days 2019 conference to give a talk “Function Totality: Abstraction Tool in Programming” and a workshop “Introduction to Dependent Types”. The talk had examples in Haskell and Idris while the workshop was in Agda. Both the talk and the workshop went quite well and I received nice comments for both. I was fortunate to have David Turner and John Hughes at my talk and to have a discussion with them around the topic.

The talk was recorded and if you’re interested in watching it, you can find it available online. Talk slides are available too.

Gave a Talk: Terminating and Productive Functions

Courtesy of Tomislav Grospić

At the Lambda Zagreb Meetup this Monday I gave a talk on terminating and productive functions. It was an interesting discussion with questions that tied the topic and examples I had with natural numbers, linear types and communicating systems.

Continue reading

Gave a Talk on Function Totality

As announced last week, yesterday I gave a talk on function totality at the Institute of Electrical and Electronics Engineers, Croatian Section. The talk was located at the University of Zagreb at the Faculty of Electrical Engineering and Computing. Slides used during the talk are freely available. The talk was in Croatian.

Continue reading

Function Totality: Abstraction Tool in Programming

Edsger Dijkstra said the following of abstraction:

“The purpose of abstraction is not to be vague, but to create a new semantic level in which one can be absolutely precise.”

Abstraction is a cornerstone of programming a complex software system. Without it, a complex software system is a complicated software system. In this article I will explore an important tool in achieving abstraction in programming: function totality.

Continue reading

Hooked on Dependent Types

Just this morning these two books landed my mailbox:

The Littler Typer and Verified Functional Programming in Agda

The Little Typer is a new book on dependent type theory, written by Daniel P. Friedman, an author of The Little Schemer, and David Thrane Christiansen, an Idris contributor. Verified Functional Programming in Agda is a book by Aaron Stump, on using dependent types in Agda to prove various properties of programs. After having read the Type-driven Development with Idris book by Edwin Brady, I am hoping these two books will significantly expand my knowledge of and improve my skills in type theory, theorem proving and typed functional programming. Looking forward to reading the books! If you haven’t noticed by now, I got hooked on dependent types!

Typed Functional Programming and Software Correctness

Software testing has been an important, if not prevalent way of checking software correctness. In this article I will tell how have my doctoral dissertation on testing and verification of imperative software as well as my work experience after the studies led me to typed functional programming, which consequently gave me a different perspective on automatic software testing. Furthermore, I’ll explain why functional programming and static type systems are important for software correctness.

Continue reading

Totality in Programming

You might think it’s only imperative programmers that don’t see value in function totality, but neither do many functional programmers. The ability to abstract in programming is severely impaired when totality is ignored. A programmer should strive to work in a programming language with a compiler that supports totality checking, such as Agda and Idris.