Stlc

The simply typed lambda-calculus (STLC) is a tiny core calculus embodying the key concept of functional abstraction. The STLC lives in the lower-left front corner of the famous lambda cube (also called the Barendregt Cube). The STLC is built on some collection of base types: booleans, numbers, strings, etc. For this chapter we just take Bool. We add boolean constants, conditionals, then the lambda calculus part: variables, function abstractions, and application. We then formalize the syntax of STLC. Types are simply boolean or arrow. The small-step semantics of STLC begins by defining the set of values - function abstractions and boolean constants are values. Then we define the notions of free variables and substitution. Substitution is in the heart of STLC. There is a short discussion of substitution here, but we should refer to PFPL’s treatment of substitution instead. After defining substitution, we define the small-step reduction: reduce the left hand side (function abstraction), reduce the right hand side (the argument), then subsitute the argument for the bound variable in the body of the function abstraction. This is called beta-reduction. We can use the normalize tactic defined in Smallstep to prove some beta-reduction examples. We extend the typing relation |--t \in T with a typing context: Gamma |--t \in T.

The rest of this book deals with STLC. We have StlcProp, MoreStlc, Subtyping Sub, Typechecker for STLC Typechecking, Records for STLC Records, etc.

The whole book feels similar to content from the first half of 15312. It might be pedagogical to revisit this book when I TA 15312.

Back to Top