Crash Course on Notation in Programming Language Theory (Part 2)
summary
Clear, hands‑on coverage of the notation you actually need: grammars for syntax, sets/tuples/relations and inductive definitions, worked big-step and small-step operational semantics with concrete derivations, a simple type safety proof sketch for an int/bool language, and exercises that extend evaluation and typing to pairs. Slides point to Pierce’s Types and Programming Languages, a blog post with pitfalls, and notes about mechanization in Coq/Isabelle. Expect specific rules, derivation trees, and which semantics are deterministic, not vague examples.
AI-written summary · about
chapters (18)
- 0:00Start
- 6:07Limitations of a Context-Free Grammar
- 6:32Operational Semantics
- 8:46Big Step Semantics
- 10:23Rule for Negation
- 10:42Negation
- 11:26Rule for Addition
- 15:37Termination
- 19:34Small Step Semantics
- 20:42Negation Rule
- 22:11Closures
- 23:32Addition
- 30:24Semantics
- 49:38Type System
- 55:16Formulations of Type Safety
- 57:44Suggested Reading
- 58:00Books That I Recommend
- 1:00:37Efficiency
related talks
01h 34mFormal Logic Undressed
52mType Theory and its Meaning Explanations
52mWhat logic can teach us, Scala programmers
42mProgramming with Math
15mLogic Programming with Extensible Types (Lightning talk)
58mKeynote: Why Functional Programming Matters
30mILLOGICAL ENGINEERS
41mPrograms and Proofs — Dependent Typing as a Way to Structure Your Code