Surface Languages
Small source-language walkthroughs built over HOAS, refinements, diagnostics, and generated data.
Surface-language examples build a simply typed lambda calculus in layers. The core syntax introduces functions and application; later pages add products, sums, recursive lists, refinements, and diagnostics.
The source for this section lives under examples/.
Walkthroughs
- Surface STLC: Surface-language walkthroughs for a simply typed lambda calculus.
Surface STLC
Surface-language walkthroughs for a simply typed lambda calculus.
STLC Core Surface
A simply typed lambda-calculus surface over the HOAS kernel.
STLC Sums and Products
Extend the STLC surface with product and sum syntax while reusing the existing HOAS kernel.
STLC Recursive Lists
List syntax and folds over description-backed recursive data.
STLC Refinements and Diagnostics
Add refinement syntax to the STLC surface while preserving source-level diagnostic classes.