4.1. Introduction🔗

HeapLang is an untyped concurrent programming language with a heap. It is an ML-like language, sporting many of the usual constructs such as let expressions, lambda abstractions, and recursive functions. It also supports higher-order functions. The evaluation order is right to left and it is a call-by-value language.

The syntax for HeapLang is fairly standard, but there are some quirks as we are working inside Lean. As the features of HeapLang are fairly standard, the focus in this chapter is mainly on showcasing the syntax of the language through simple examples.

The Lean port of HeapLang in iris-lean differs from the Rocq version in two notable ways:

1. Expressions live in the type Iris.HeapLang.Exp, and are written inside an embedded DSL hl( ... ) rather than via top-level notation. Values are inside hl_val(...).

2. Variable names are still strings underneath, but you do not need to quote them: write x rather than "x".