An implementation of the IMP language from "The Formal Semantics of Programming Languages" with a REPL environment.

IMP is a small language of while programs. IMP is called an "imperative" language because program execution involves carrying out a series of explicit commands to change state. Formally, IMP's behaviour is described by rules which specify how its expressions are evaluated and its commands are executed.

Currently, there is no pre-build binaries.

To build and run the REPL, execute:

stack build --exec IMP-lang-exe

a ::= n | X | a + a | a - a | a × a

b ::= true | false | a = a | a ≤ a | ¬b | b ∧ b | b ∨ b

c ::= skip | X := a | c;c | if b then c else c | while b do c

• Aexp

  ⊢ <n, σ> → n

  ⊢ <X, σ> → σ(X)

  <a₀, σ> → n₀, <a₁, σ> → n₁ ⊢ <a₀ + a₁, σ> → n (if n = n₀ + n₁)

  <a₀, σ> → n₀, <a₁, σ> → n₁ ⊢ <a₀ - a₁, σ> → n (if n = n₀ - n₁)

  <a₀, σ> → n₀, <a₁, σ> → n₁ ⊢ <a₀ × a₁, σ> → n (if n = n₀ × n₁)

• Bexp

  ⊢ <true, σ> → true

  ⊢ <false, σ> → false

  <a₀, σ> → n, <a₁, σ> → m ⊢ <a₀ = a₁, σ> → true (if n ≡ m)

  <a₀, σ> → n, <a₁, σ> → m ⊢ <a₀ = a₁, σ> → false (if n ≠ m)

  <a₀, σ> → n, <a₁, σ> → m ⊢ <a₀ ≤ a₁, σ> → true (if n ≤ m)

  <a₀, σ> → n, <a₁, σ> → m ⊢ <a₀ ≤ a₁, σ> → false (if n > m)

  <b, σ> → true ⊢ <¬b, σ> → false

  <b, σ> → false ⊢ <¬b, σ> → true

  <b₀, σ> → t₀, <b₁, σ> → t₁ ⊢ <b₀ ∧ b₁, σ> → t (t = true if t₀ ≡ true and t₁ ≡ true, otherwise t = false)

  <b₀, σ> → t₀, <b₁, σ> → t₁ ⊢ <b₀ ∨ b₁, σ> → t (t = true if t₀ ≡ true or t₁ ≡ true, otherwise t = false)

• Com

  ⊢ <skip, σ> → σ

  <a, σ> → m ⊢ <X := a, σ> → σ[m/X]

  <c₀, σ> → σ'', <c₁, σ''> → σ' ⊢ <c₀;c₁, σ> → σ'

  <b, σ> → true, <c₀, σ> → σ' ⊢ <if b then c₀ else c₁, σ> → σ'

  <b, σ> → false, <c₁, σ> → σ' ⊢ <if b then c₀ else c₁, σ> → σ'

  <b, σ> → false ⊢ <while b do c, σ> → σ

  <b, σ> → true, <c, σ> → σ'', <while b do c, σ''> → σ' ⊢ <while b do c, σ> → σ'