This page contains various materials for the PL course
Invitation for the SLACK workspace
Shared Folder with Sample Code
SASyLF Proof Assistant @ Carnegie Mellon
Slides of Recitation Lectures and Bibliographic pointers
Module 1 (30-Abr-2025)
Other references:
(Church's Lambda Calculus - notes by Robert Harper, CMU )
(Programming Languages and Lambda Calculi, book by Mathias Felleisen, see Chapter 5)
(Chapter 5 The Untyped Lambda-Calculus, Types and Programming Languages, book by Benjamin Pierce)
Module 2 (6-May-2025) [ last update 13MAY16:00]
Module 3 (7-May-2025) [ last update 13MAY16:00](Chapter 13 References, Types and Programming Languages, book by Benjamin Pierce)
Module 4 (13-May-2025) [ last update 13MAY16:00]Other references:
(Type Systems - overview by Luca Cardelli)
(Chapter 9 Simply Typed Lambda-Calculus, Types and Programming Languages, book by Benjamin Pierce)
Module 5 (14-May-2025) [ last update 14MAY13:00]
(Chapter 9 Simply Typed Lambda-Calculus, Types and Programming Languages, book by Benjamin Pierce)
Module 6 (20-May-2025) [ last update 20MAY16:00]
Module 7 (21-May-2025) [ last update 19MAY13:00]
Module 8 (27-May-2025) [ last update 26MAY13:00]
(A shorthand intro to inductive types and induction proofs - Excerpt From Aldrich CMU notes)
Live session, see drive for SasyLF scripts.
Live session, see drive for SasyLF scripts.
Module 10 (3-Jun-2025) [ last update 2Jun19:00]
Live session, see drive for SasyLF scripts.
Module 11 (4-Jun-2025) [ last update 4Jun14:45]
Module 10 (3-Jun-2025) [ last update 2Jun19:00]
Live session, see drive for SasyLF scripts.
Module 11 (4-Jun-2025) [ last update 4Jun14:45]
Live session, see drive for SasyLF scripts.
L1 - Programming in the Lambda-calculus.
L2 - Booting up Project Phase 1 (Step 1).
L3 - Booting up Project Phase 1 (Step 2).
L4 - Basic PL ConceptsL5 - Support to Project Phase 1L6 - Solution of Demo MAP test
L7 - Structural InductionL8 - SASyLF basic induction proofs (all guides)L8-9 - SASyLF structural induction proofs (all guides)
L10-11 SASyLF structural induction proofs (all guides)
Programming Language Semantics
Interpreters
Lambda Calculus (Module 1)
Operational Semantics, Small Step, Big Step (Module 2,3)
Type Systems (Module 4)
Closures (Module 2)
References (Module 3)
Abstract Syntax Tree (Recap)
Module 12 (11-Jun-2025) [ last update 4Jun14:45]
LAB guides
L1 - Programming in the Lambda-calculus.
L2 - Booting up Project Phase 1 (Step 1).
L3 - Booting up Project Phase 1 (Step 2).
L4 - Basic PL ConceptsL5 - Support to Project Phase 1L6 - Solution of Demo MAP test
L7 - Structural InductionL8 - SASyLF basic induction proofs (all guides)L8-9 - SASyLF structural induction proofs (all guides)
L10-11 SASyLF structural induction proofs (all guides)
Complementary Quick (and sound) Links at Wikipedia
General
Programming Language Semantics
Interpreters
Specific
Lambda Calculus (Module 1)
Operational Semantics, Small Step, Big Step (Module 2,3)
Type Systems (Module 4)
Closures (Module 2)
References (Module 3)
Abstract Syntax Tree (Recap)