The lambda-Calculus: from Simple Types to non-Idempotent Intersection Types
An introductory course for ECI 2024 (Buenos Aires, Argentina, 29 July-2 August 2024), by Giulio Guerrieri.
- Day 1: Natural deduction for minimal logic and cut-elimination.
Slides
- Day 2: The simply typed lambda-calculus and the Curry-Howard correspondence. Slides
- Day 3: The untyped lambda-calculus. Slides
- Day 4: Non-idempotent intersection types for the lambda-calculus. Slides
- Day 5: More on non-idempotent intersection types for the lambda-calculus. Slides
- Solutions to selected exercises from Days 1-5. Pdf
- Final exam. Pdf
- Solutions to exam exercises. Pdf
What some students said about this course:
- I really liked the course!
- Thank you for the lectures!
- Thank you for the course. It was very good.
- I really enjoyed the course and it was really interesting, thank you!
- I really enjoyed your course. I took three courses during the ECI (morning, afternoon, and evening), and yours was the one I liked the most. I believe you did an excellent job of conveying the material.
- I think I speak for every student who took your classes when I say that it was an excellent class, incredibly explanatory and hella funny. It was my first time taking an ECI class, but other students who took ECIs classes before would tell you the same things I'm saying. It really enlightened me about how crazy and important lambda-calculus really is for computer science.