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!
Benjamin C. Pierce writes what it is like to use a proof assistant to teach programming language foundations.
Philip Wadler makes a fun note about today’s programming languages: “Most of you use programming languages that are invented, and you can tell, can’t you?” I recommend watching his whole talk Propositions as Types!