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.
On February 6 in Zagreb I’ll be giving a talk on the role of types in programming as part of the Lambda Zagreb group. It will be about pushing the domain into types. I’ll cover various topics, including dependent types and refinement types. An example that I’ll give and that will hopefully be most interesting is about encoding a state machine at the type level. This means that if you try to make an illegal state transition in the code, it won’t compile. My code snippets are going to be in Idris, but I’ll provide Haskell and Scala equivalents where applicable.
The talk is going to be in Croatian, but I’ll do my best to have the slide deck ready in English just in case.