Crash Course on Notation in Programming Language Theory (Part 1)
summary
Crash course promises concrete mechanics: reading POPL/ICFP notation by building inductive definitions with base cases and rules, drawing derivation trees, writing BNF-style grammars and the PL convention that metavariables stand for ranges, and a hands-on introduction to operational semantics plus a possible type safety proof. Expect short exercises, explicit rules-of-thumb about negation and fixed points, and worked examples that show how to justify or refute specific membership and typing claims.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 5:12Sets
- 9:15tuples
- 10:15relations
- 13:35rules
- 18:20nonsensical rules
- 21:50horizontal lines
- 25:51derivation
- 28:58exercises
- 30:32even
- 40:15Syntax
- 52:09Exercise
related talks
01h 07mInvited Talk - Guy Steele
02h 50mIntro to Type Systems and Operational Semantics
01h 34mFormal Logic Undressed
49mFunctional Programming Essentials
22mA Calculus of Inductive Linear Constructions
58mKeynote: Why Functional Programming Matters
12mOn the power of syntactic methods: It is all syntax after all…
35mUsing the Design Recipe in Theory of Computation