BFPG Meetup - February 2025 - Explicit substitutions + Mentor networking session

​Agenda

• ​18:00: Welcome and setup

• ​Presentation #1: Lambda calculi with explicit substitutions - Donovan Crichton

• ​Presentation #2: Mentor networking session - hosted by Jack Kelly

• ​20:00ish: Pack down, head to Criterion pub.

​Lambda calculi with explicit substitutions

​Explicit substitutions are a commonly encountered extension to typed lambda calculi - particularly when working with higher order, or dependently typed variants. This talk will cover the rationale, syntax and evaluation for explicit substitutions, and showcase how they reduce the burden of reasoning about the substitution operation in the meta-theory.

​We will undertake a tour of the following concepts that are suitable for beginner functional programmers: Simply Typed Lambda Calculus, de Bruijn Indices, and typing rule notation. We will conclude with a mutually inductive presentation of explicit substitution over a dependent type theory for more advanced attendees.

​Mentor networking session

​Have you decided that 2025 is the year you learn FP? Do you have a project in mind, but you don't know where to start? Do you have skills to share and a bit of free time?

​We're inviting people to briefly talk about things they want to share and want to learn about in the FP world: languages, tools, techniques, libraries, projects. We want to help mentors and mentees find each other and hopefully kick off some new conversations at the pub.