Examples

Lambda Calculi

• Tutorial language: Lambda calculus with syntactic additions and typing added in an extension
• Simply-typed lambda calculus: Simply-typed lambda calculus with syntactic extensions

Imperative Languages

• Simple imperative language: Imperative language with statements and expressions with syntactic and semantic additions
• Functions: Imperative language with function calls, statements, and expressions with syntactic and semantic additions

Other

• UNSAT proofs: Language for proving CNF problems are unsatisfiable with syntactic and semantic additions

Modeling Other Extensibility Frameworks

• Modular structural operational semantics: MSOS allows adding effects to languages in extensions
• Meta-Theory a la Carte: MTC uses a set of shared declarations, with extensions adding definitions of these declarations
• SoundX: SoundX allows extensions to introduce new typing rules, but defines evaluation for the host language alone

Tarball of all examples (Tarballs of individual examples available on their respective pages)