On Tuesday, March 26, I’ll be giving a talk on propositions as types to the Lambda Zagreb Meetup group. The talk will be in Croatian and it is titled ¬ sve za ∀ (no ∃ uvod u propozicije kao tipove), which can be translated as ¬ everything is for ∀ (but there ∃ an introduction to propositions as types). Obviously, I incorporated logic operators into the title with the goal to make it catchy and to attract more audience with an unusual title. Given that only about 10 people RSVPed so far and that there are only three days left until the talk, it looks like I’ve achieved quite the opposite!
In the talk I will glance over the first half of the book Programming Language Foundations in Agda by Wadler and Kokke, which is about logic and how to represent it via programs in Agda. I’m going to to give an introduction to propositions as types (an idea also known as the Curry-Howard correspondence and by many other names) and motivate people to think in terms of types instead of sets when writing programs. Although few programming languages have as advanced type system as Agda does, I’ll give guidance to what can be done in languages like Haskell to program in a type-theoretic way rather than in a set-theoretic way.