Part 1: Defining LAMBDA

Here you will learn how to define a very simple language in K and the basics of how to use the K tool. The language is a variant of call-by-value lambda calculus and its definition is based on substitution. Specifically, you will learn the following:

  • How to define a module.
  • How to define a language syntax.
  • How to use the defined syntax to parse programs.
  • How to import predefined modules.
  • How to define evaluation strategies using strictness attributes.
  • How to define semantic rules.
  • How the predefined generic substitution works.
  • How to generate PDF and HTML documentation from ASCII definitions.
  • How to include builtins (integers and Booleans) into your language.
  • How to define derived language constructs.

This folder contains several lessons, each adding new features to LAMBDA.