The lambda-calculus: from simple types to non-idempotent intersection types

An introductory course for ESSLLI 2023 (Ljubljana, Slovenia, 7-11 August 2023), by Giulio Guerrieri.

• Days 1-2: The simply typed lambda-calculus and the Curry-Howard correspondence. Slides
• Day 3: The untyuped lambda-calculus. Slides
• Days 4-5: Non-idempotent intersection types for the lambda-calculus. Slides