diff --git a/Strata/Languages/Laurel/Examples/Allocation.lr.st b/Strata/Languages/Laurel/Examples/Allocation.lr.st
new file mode 100644
index 00000000..61bda2f3
--- /dev/null
+++ b/Strata/Languages/Laurel/Examples/Allocation.lr.st
@@ -0,0 +1,82 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+-- WIP. needs further design
+
+-- Create immutable composite
+composite Immutable {
+  val x: int
+  val y: int
+
+  invariant x + y >= 5
+
+  val construct = procedure()
+    constructor
+    requires contructing == {this}
+    ensures constructing == {}
+  {
+    x = 3; -- we can assign to an immutable field, while the target is in the constructing set.
+    y = 2;
+    construct this; -- checks that all fields of 'this' have been assigned
+  }
+}
+
+val foo = procedure() {
+  val immutable = Immutable.construct(); -- constructor instance method can be called as a static.
+}
+
+-- Create immutable circle
+composite ImmutableChainOfTwo {
+  val other: ChainOfTwo -- note the field is immutable
+
+  invariant other.other == this -- reading other.other is allowed because the field is immutable
+
+  val construct = constructor() 
+    requires contructing == {this}
+    ensures constructing == {}
+  {
+    var second = allocate();
+    assert constructing == {this, second};
+
+    second.other = first; -- we can assign to a mutable field because second is in the constructing set
+    first.other = second;
+    construct first;
+    construct second;
+  }
+
+  -- only used privately
+  val allocate = constructor()
+    ensures constructing = {this} {    
+    -- empty body
+  }
+}
+
+val foo2 = procedure() {
+  val immutable = ImmutableChainOfTwo.construct();
+  val same = immutable.other.other;
+  assert immutable =&= same;
+}
+
+-- Helper constructor
+composite UsesHelperConstructor {
+  val x: int
+  val y: int
+
+  val setXhelper = constructor() 
+    requires constructing == {this}
+    ensures constructing == {this} && assigned(this.x)
+  {
+    this.x = 3;
+  }
+
+  val construct = constructor() 
+    requires contructing == {this}
+    ensures constructing == {}
+  {
+    this.setXhelper();
+    y = 2;
+    construct this;
+  }
+}
\ No newline at end of file
diff --git a/Strata/Languages/Laurel/Examples/ConstrainedTypes.lr.st b/Strata/Languages/Laurel/Examples/ConstrainedTypes.lr.st
new file mode 100644
index 00000000..278ed6ba
--- /dev/null
+++ b/Strata/Languages/Laurel/Examples/ConstrainedTypes.lr.st
@@ -0,0 +1,15 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+-- Constrained primitive type
+constrained nat = x: int where x >= 0
+
+-- Something analogous to an algebriac datatype
+composite OptionBase {}
+composite Some extends OptionBase { 
+  value: int
+}
+composite None extends OptionBase
+constrained Option = x: OptionBase where x is Some || x is None
\ No newline at end of file
diff --git a/Strata/Languages/Laurel/Examples/InstanceCallables.lr.st b/Strata/Languages/Laurel/Examples/InstanceCallables.lr.st
new file mode 100644
index 00000000..293e1281
--- /dev/null
+++ b/Strata/Languages/Laurel/Examples/InstanceCallables.lr.st
@@ -0,0 +1,31 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+composite Base {
+  procedure foo(): int
+    ensures result > 3
+    { abstract }
+}
+
+composite Extender1 extends Base {
+  procedure foo(): int
+    ensures result > 4
+--  ^^^^^^^ error: could not prove ensures clause guarantees that of extended method 'Base.foo'
+    { abstract }
+}
+
+composite Extender2 extends Base {
+  value: int
+  procedure foo(): int
+    ensures result > 2
+  {
+    this.value + 2 -- 'this' is an implicit variable inside instance callables
+  }
+}
+
+val foo = procedure(b: Base) {
+  var x = b.foo();
+  assert x > 3; -- pass
+}
\ No newline at end of file
diff --git a/Strata/Languages/Laurel/Examples/Jumps.lr.st b/Strata/Languages/Laurel/Examples/Jumps.lr.st
new file mode 100644
index 00000000..4182afd6
--- /dev/null
+++ b/Strata/Languages/Laurel/Examples/Jumps.lr.st
@@ -0,0 +1,26 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+val forLoopLikeWithBreakAndContinue = procedure(steps: int, continueSteps: int, exitSteps: int): int {
+  var counter = 0
+  breakLabel {
+    while(steps > 0) 
+      invariant counter >= 0
+    {
+      continueLabel {
+        if (steps == exitSteps) {
+          counter = -10;
+          exit breakLabel;
+        }
+        if (steps == continueSteps) {
+          exit continueLabel;
+        }
+        counter = counter + 1
+      }
+      steps = steps - 1;
+    }
+  }
+  counter;
+}
\ No newline at end of file
diff --git a/Strata/Languages/Laurel/Examples/PureAllocation.lr.st b/Strata/Languages/Laurel/Examples/PureAllocation.lr.st
new file mode 100644
index 00000000..9d493312
--- /dev/null
+++ b/Strata/Languages/Laurel/Examples/PureAllocation.lr.st
@@ -0,0 +1,26 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+-- WIP. needs further design
+composite Immutable {
+  val x: int
+
+  val construct = function(): pure Immutable
+    constructor
+    requires constructing = {this}
+    ensures constructing == {}
+  {
+    this.x = 3;
+    construct this;
+    this
+  }
+}
+
+val pureCompositeAllocator = function(): boolean {
+  var i: pure Empty = Immutable.construct(); -- can be called in a pure construct, because it is a function
+  var j: pure Empty = Immutable.construct();
+  i =&= j
+--  ^^^ reference equality operator '=&=' can not be used on pure types
+}
\ No newline at end of file
diff --git a/Strata/Languages/Laurel/Examples/ReadsAndModifiesClauses.lr.st b/Strata/Languages/Laurel/Examples/ReadsAndModifiesClauses.lr.st
new file mode 100644
index 00000000..338153d6
--- /dev/null
+++ b/Strata/Languages/Laurel/Examples/ReadsAndModifiesClauses.lr.st
@@ -0,0 +1,59 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+composite Container {
+  var value: int
+}
+
+val permissionLessReader = function(c: Container): int
+  { c.value }
+--  ^^^^^^^ error: enclosing function 'permissionLessReader' does not have permission to read 'c.value'
+
+val varReader = function(c: Container): int
+  reads c
+  { c.value }
+
+composite ImmutableContainer {
+  val value: int
+}
+
+val valReader = function(c: ImmutableContainer): int
+  { c.value } -- no reads clause needed because value is immutable
+
+val opaqueFunction = function(c: Container): int
+  reads c
+  ensures true 
+  { 3 }
+
+val foo = procedure(c: Container, d: Container) 
+{
+  var x = opaqueFunction(c);
+  modifyContainer(d);
+  var y = opaqueFunction(c);
+  assert x == y; -- functions return the same result when the arguments and read objects are the same
+  modifyContainer(c);
+  c.value = c.value + 1;
+  var z = opaqueFunction(c);
+  assert x == z;
+--         ^^ error: could not prove assert
+}
+
+val modifyContainer(c: Container) 
+  modifies c
+{
+  c.value = c.value + 1;
+}
+
+val modifyContainerWithoutPermission(c: Container) 
+{
+  c.value = c.value + 1;
+--        ^ error: enclosing function 'modifyContainerWithoutPermission' does not have permission to modify 'c.value'
+}
+
+-- Pure types
+val impureTypeUser = function(i: pure Container, j: pure Container): boolean {
+  i =&= j
+--  ^^^ reference equality operator '=&=' can not be used on pure types
+}
\ No newline at end of file
diff --git a/Strata/Languages/Laurel/Examples/StmtExpr.lr.st b/Strata/Languages/Laurel/Examples/StmtExpr.lr.st
new file mode 100644
index 00000000..d34dd24a
--- /dev/null
+++ b/Strata/Languages/Laurel/Examples/StmtExpr.lr.st
@@ -0,0 +1,37 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+function nesting(a: int): int
+  requires a > 0 && a < 100
+  returns
+{
+  var b = a + 2;
+  if (b > 2) {
+      var c = b + 3;
+      if (c > 3) {
+          return c + 4;
+      }
+      var d = c + 5;
+      return d + 6;
+  }
+  var e = b + 1;
+  e
+}
+
+composite Counter {
+  var value: int
+}
+
+int nestedImpureCalls(counter: Counter) {
+    if (add(counter, 1) == 1) {
+        var x = add(counter, add(counter, 2));
+        return x;
+    }
+    return add(counter, 3);
+}
+
+method add(counter: Counter, amount: int): int {
+  counter.value = counter.value + amount
+}
\ No newline at end of file
diff --git a/Strata/Languages/Laurel/Examples/TypeTests.lr.st b/Strata/Languages/Laurel/Examples/TypeTests.lr.st
new file mode 100644
index 00000000..c3ce5f9d
--- /dev/null
+++ b/Strata/Languages/Laurel/Examples/TypeTests.lr.st
@@ -0,0 +1,26 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+composite Base {
+  var x: int
+}
+
+composite Extended1 extends Base {
+  var y: int
+}
+
+composite Extended2 extends Base {
+  var z: int
+}
+
+val typeTests = procedure(e: Extended1) {
+  var b: Base = e as Base; -- even upcasts are not implicit, but they pass statically
+  var e2 = e as Extended2;
+--           ^^ error: could not prove 'e' is of type 'Extended2'
+  if (e is Extended2) {
+    -- unreachable, but that's OK
+    var e2pass = e as Extended2; -- no error
+  }
+}
\ No newline at end of file
diff --git a/Strata/Languages/Laurel/Laurel.lean b/Strata/Languages/Laurel/Laurel.lean
new file mode 100644
index 00000000..8aaefe9c
--- /dev/null
+++ b/Strata/Languages/Laurel/Laurel.lean
@@ -0,0 +1,245 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+/-
+The Laurel language is supposed to serve as an intermediate verification language for at least Java, Python, JavaScript.
+
+It enables doing various forms of verification:
+- Deductive verification
+- Property based testing
+- Data-flow analysis
+
+Features currently not present:
+- Type inference. The source program needs to specify enough types so that no inference is needed.
+- Type checking. We assume types have already been checked before.
+- Namespaces. All definition and reference names consist of a single Identifier
+
+Design choices:
+- Pure contracts: contracts may only contain pure code. Pure code does not modify the heap, neither by modifying existing objects are creating new ones.
+- Callables: instead of functions and methods we have a single more general concept called a 'callable'.
+- Purity: Callables can be marked as pure or impure. Pure callables have a reads clause while impure ones have a modifies clause.
+  A reads clause is currently not useful for impure callables, since reads clauses are used to determine when the output changes, but impure callables can be non-determinismic so the output can always change.
+- Opacity: callables can have a body that's transparant or opaque. Only an opaque body may declare a postcondition. A transparant callable must be pure.
+- StmtExpr: Statements and expressions are part of the same type. This reduces duplication since the same concepts are needed in both, such as conditions and variable declarations.
+- Loops: The only loop is a while, but this can be used to compile do-while and for loops to as well.
+- Jumps: Instead of break and continue statements, there is a labelled block that can be exited from using an exit statement inside of it.
+  This can be used to model break statements and continue statements for both while and for loops.
+
+- User defined types consist of two categories: composite types and constrained types.
+- Composite types have fields and callables, and may extend other composite types.
+  - Fields state whether they are mutable, which impacts what permissions are needed to access them
+  - Fields state their type, which is needed to know the resulting type when reading a field.
+- Constrained types are defined by a base type and a constraint over that type.
+  - Algebraic datatypes do not exist directly but can be encoded using composite and constrained types.
+
+- For now there is no type polymorphism
+
+- Construction of composite types is WIP. It needs a design first.
+
+-/
+
+abbrev Identifier := String /- Potentially this could be an Int to save resources. -/
+
+mutual
+structure Callable: Type where
+  name : Identifier
+  inputs : List Parameter
+  output : HighType
+  precondition : StmtExpr
+  decreases : StmtExpr
+  purity : Purity
+  body : Body
+
+structure Parameter where
+  name : Identifier
+  type : HighType
+
+inductive HighType : Type where
+  | TVoid
+  | TBool
+  | TInt
+  | TFloat64 /- Required for JavaScript (number). Used by Python (float) and Java (double) as well -/
+  | UserDefined (name: Identifier)
+  | Applied (base : HighType) (typeArguments : List HighType)
+  /- Pure represents a composite type that does not support reference equality -/
+  | Pure(base: HighType)
+  /- Java has implicit intersection types.
+     Example: `<cond> ? RustanLeino : AndersHejlsberg` could be typed as `Scientist & Scandinavian`-/
+  | Intersection (types : List HighType)
+  deriving Repr
+
+inductive Purity: Type where
+/-
+Since a reads clause is used to determine when the result of a call changes,
+a reads clause is only useful for deterministic callables.
+-/
+  | Pure (reads : StmtExpr)
+  | Impure (modifies : StmtExpr)
+
+/- No support for something like function-by-method yet -/
+inductive Body where
+  | Transparent (body : StmtExpr)
+/- Without an implementation, the postcondition is assumed -/
+  | Opaque (postcondition : StmtExpr) (implementation : Option StmtExpr)
+/- An abstract body is useful for types that are extending.
+    A type containing any members with abstract bodies can not be instantiated. -/
+  | Abstract (postcondition : StmtExpr)
+
+/- We will support these operations for dynamic types as well -/
+/- The 'truthy' concept from JavaScript should be implemented using a library function -/
+inductive Operation: Type where
+  /- Works on Bool -/
+    /- Equality on composite types uses reference equality for impure types, and structural equality for pure ones -/
+  | Eq | Neq
+  | And | Or | Not
+  /- Works on Int/Float64 -/
+  | Neg | Add | Sub | Mul | Div | Mod
+  | Lt | Leq | Gt | Geq
+
+/-
+A StmtExpr contains both constructs that we typically find in statements and those in expressions.
+By using a single datatype we prevent duplication of constructs that can be used in both contexts,
+such a conditionals and variable declarations
+-/
+/-
+It would be nice to replace `Type` on the next line with `(isPure: Bool) -> Type`,
+so that we can prevent certain constructors from being used for pure StmtExpr's,
+but when trying that Lean complained about parameters being used in a nested inductive,
+for example in `Option (StmtExpr isPure)`
+-/
+inductive StmtExpr : Type where
+/- Statement like -/
+  | IfThenElse (cond : StmtExpr) (thenBranch : StmtExpr) (elseBranch : Option StmtExpr)
+  | Block (statements : List StmtExpr) (label : Option Identifier)
+  /- The initializer must be set if this StmtExpr is pure -/
+  | LocalVariable (name : Identifier) (type : HighType) (initializer : Option StmtExpr)
+  /- While is only allowed in an impure context
+    The invariant and decreases are always pure
+  -/
+  | While (cond : StmtExpr) (invariant : Option StmtExpr) (decreases: Option StmtExpr) (body : StmtExpr)
+  | Exit (target: Identifier)
+  | Return (value : Option StmtExpr)
+/- Expression like -/
+  | LiteralInt (value: Int)
+  | LiteralBool (value: Bool)
+  | Identifier (name : Identifier)
+  /- Assign is only allowed in an impure context -/
+  | Assign (target : StmtExpr) (value : StmtExpr)
+  /- Used by itself for fields reads and in combination with Assign for field writes -/
+  | FieldSelect (target : StmtExpr) (fieldName : Identifier)
+  /- PureFieldUpdate is the only way to assign values to fields of pure types -/
+  | PureFieldUpdate (target : StmtExpr) (fieldName : Identifier) (newValue : StmtExpr)
+  | StaticCall (callee : Identifier) (arguments : List StmtExpr)
+  | PrimitiveOp (operator: Operation) (arguments : List StmtExpr)
+/- Instance related -/
+  | This
+  | ReferenceEquals (lhs: StmtExpr) (rhs: StmtExpr)
+  | AsType (target: StmtExpr) (targetType: HighType)
+  | IsType (target : StmtExpr) (type: HighType)
+  | InstanceCall (target : StmtExpr) (callee : Identifier) (arguments : List StmtExpr)
+
+/- Verification specific -/
+  | Forall (name: Identifier) (type: HighType) (body: StmtExpr)
+  | Exists (name: Identifier) (type: HighType) (body: StmtExpr)
+  | Assigned (name : StmtExpr)
+  | Old (value : StmtExpr)
+  /- Fresh may only target impure composite types -/
+  | Fresh(value : StmtExpr)
+
+/- Related to proofs -/
+  | Assert (condition: StmtExpr)
+  | Assume (condition: StmtExpr)
+  /-
+ProveBy allows writing proof trees. Its semantics are the same as that of the given `value`,
+but the `proof` is used to help prove any assertions in `value`.
+Example:
+ProveBy(
+  someCall(arg1, arg2),
+  ProveBy(
+    aLemmaToHelpProveThePreconditionOfTheCall(),
+    anotherLemmaToProveThePreconditionOfTheFirstLemma()
+  )
+)
+-/
+  | ProveBy (value: StmtExpr) (proof: StmtExpr)
+
+-- ContractOf allows extracting the contract of a function
+  | ContractOf (type: ContractType) (function: StmtExpr)
+/-
+Abstract can be used as the root expr in a contract for reads/modifies/precondition/postcondition. For example: `reads(abstract)`
+It can only be used for instance callables and it makes the containing type abstract, meaning it can not be instantiated.
+An extending type can become concrete by redefining any callables that had abstracts contracts and providing non-abstract contracts.
+-/
+  | Abstract
+  | All -- All refers to all objects in the heap. Can be used in a reads or modifies clause
+/- Hole has a dynamic type and is useful when programs are only partially available -/
+  | Hole
+
+inductive ContractType where
+  | Reads | Modifies | Precondition | PostCondition
+end
+
+partial def highEq (a: HighType) (b: HighType) : Bool := match a, b with
+  | HighType.TVoid, HighType.TVoid => true
+  | HighType.TBool, HighType.TBool => true
+  | HighType.TInt, HighType.TInt => true
+  | HighType.TFloat64, HighType.TFloat64 => true
+  | HighType.UserDefined n1, HighType.UserDefined n2 => n1 == n2
+  | HighType.Applied b1 args1, HighType.Applied b2 args2 =>
+      highEq b1 b2 && args1.length == args2.length && (args1.zip args2 |>.all (fun (a1, a2) => highEq a1 a2))
+  | HighType.Intersection ts1, HighType.Intersection ts2 =>
+      ts1.length == ts2.length && (ts1.zip ts2 |>.all (fun (t1, t2) => highEq t1 t2))
+  | _, _ => false
+
+instance : BEq HighType where
+  beq := highEq
+
+def HighType.isBool : HighType → Bool
+  | TBool => true
+  | _ => false
+
+structure Field where
+  name : Identifier
+  isMutable : Bool
+  type : HighType
+
+structure CompositeType where
+  name : Identifier
+  /-
+  The type hierarchy affects the results of IsType and AsType,
+  and can add checks to the postcondition of callables that extend another one
+  -/
+  extending : List Identifier
+  fields : List Field
+  instanceCallables : List Callable
+
+structure ConstrainedType where
+  name : Identifier
+  base : HighType
+  valueName : Identifier
+  constraint : StmtExpr
+  witness : StmtExpr
+
+/-
+Note that there are no explicit 'inductive datatypes'. Typed unions are created by
+creating a CompositeType for each constructor, and a ConstrainedType for their union.
+
+Example 1:
+`composite Some<T> { value: T }`
+`constrained Option<T> = value: Dynamic | value is Some<T> || value is Unit`
+
+Example 2:
+`composite Cons<T> { head: T, tail: List<T> }`
+`constrained List<T> = value: Dynamic | value is Cons<T> || value is Unit`
+ -/
+inductive TypeDefinition where
+  | Composite (ty : CompositeType)
+  | Constrainted {ConstrainedType} (ty : ConstrainedType)
+
+structure Program where
+  staticCallables : List Callable
+  staticFields : List Field
+  types : List TypeDefinition
diff --git a/Strata/Languages/Laurel/LaurelEval.lean b/Strata/Languages/Laurel/LaurelEval.lean
new file mode 100644
index 00000000..fd81fc67
--- /dev/null
+++ b/Strata/Languages/Laurel/LaurelEval.lean
@@ -0,0 +1,347 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+/-
+This file defines the behavior of both a type checker and a verifier for the Laurel language.
+Both are defined using the 'eval' function. It will only return a single type or verification error at a time.
+
+TODO: implicit casting from primitives types to Dynamic
+-/
+import Strata.DL.HighStrata.HighStrata
+import Std.Data.HashMap.Basic
+import Lean.Data.AssocList
+
+namespace HighLevel
+
+open Std
+open Lean
+open HighLevel
+
+mutual
+-- Runtime values with explicit universe level
+inductive Value : Type where
+  | VUnknown : Value
+  | VVoid : Value
+  | VBool : Bool → Value
+  | VInt : Int → Value
+  -- | VReal : Rat → Value -- Skipped for now, as Lean's Rat requires importing MathLib
+  | VFloat64 : Float → Value
+  | VBoxed : TypedValue → Value
+  | VObject : (type: Identifier) → (field: AssocList Identifier Value) → Value
+  | VNull : Value
+  | VClosure : Callable → Value
+
+structure TypedValue where
+  val : Value
+  ty : HighType
+
+end
+
+instance : Inhabited TypedValue where
+  default := { val := Value.VVoid, ty := HighType.TVoid }
+
+def Value.asBool! : Value → Bool
+  | VBool b => b
+  | _ => panic! "expected VBool"
+
+def Value.asInt! : Value → Int
+  | VInt i => i
+  | _ => panic! "expected VInt"
+
+def Value.asFloat64! : Value → Float
+  | VFloat64 f => f
+  | _ => panic! "expected VFloat64"
+
+def Value.asBoxed! : Value → TypedValue
+  | VBoxed tv => tv
+  | _ => panic! "expected VBoxed"
+
+def Value.asObject! : Value → Identifier × AssocList Identifier Value
+  | VObject ty fields => (ty, fields)
+  | _ => panic! "expected VObject"
+
+-- Environment for variable bindings
+structure Env where
+  locals: List (AssocList Identifier TypedValue)
+  statics: HashMap Identifier Callable
+  heap: HashMap Int Value
+  returnType : HighType
+
+inductive VerificationErrorType : Type where
+  | PreconditionFailed : VerificationErrorType
+  | PostconditionFailed : VerificationErrorType
+  | InvariantFailed : VerificationErrorType
+  | DecreasesFailed : VerificationErrorType
+  | ReadEffectFailed : VerificationErrorType
+
+-- Evaluation result
+inductive EvalResult (value: Type u) : Type u where
+  | Success : value → EvalResult value
+  | Return : Value → EvalResult value
+  | Exitting : (target: Identifier) → EvalResult value
+  | TypeError : String → EvalResult value
+  | VerficationError : VerificationErrorType → String → EvalResult value
+
+def Eval (value: Type u): Type u := Env → EvalResult value × Env
+def getLocal (name: Identifier) : Eval TypedValue :=
+  let rec getInLocal (locals: List (AssocList Identifier TypedValue)) :=
+    match locals with
+    | [] => none
+    | top :: rest =>
+      match top.find? name with
+      | some result => some result
+      | none => getInLocal rest
+
+  fun env => match getInLocal env.locals with
+    | some result => (EvalResult.Success result, env)
+    | none => (EvalResult.TypeError s!"Undefined variable: {name}", env)
+
+def getEnv : Eval Env := fun env => (EvalResult.Success env, env)
+def setEnv (newEnv: Env) : Eval PUnit := fun _ => (EvalResult.Success PUnit.unit, newEnv)
+
+def voidTv : TypedValue :=
+  { val := Value.VVoid, ty := HighType.TVoid }
+
+def setLocal (name: Identifier) (typedValue: TypedValue): Eval PUnit :=
+  fun env => (EvalResult.Success PUnit.unit, { env with locals := (env.locals.head!.insert name typedValue :: env.locals.tail) })
+
+def pushStack: Eval PUnit :=
+  fun env => (EvalResult.Success PUnit.unit, { env with locals := AssocList.empty :: env.locals })
+def popStack: Eval PUnit :=
+  fun env => (EvalResult.Success PUnit.unit, { env with locals := env.locals.tail })
+
+def assertBool (tv: TypedValue) : Eval PUnit := fun env =>
+  if (tv.ty.isBool) then
+    (EvalResult.TypeError "Precondition must be boolean", env)
+  else if (tv.val.asBool!) then
+    (EvalResult.VerficationError VerificationErrorType.PreconditionFailed "Precondition does not hold", env)
+  else
+    (EvalResult.Success PUnit.unit, env)
+
+instance : Monad Eval where
+  pure x := fun e => (EvalResult.Success x, e)
+  bind := fun r f => fun env =>
+    let (r', env') := r env
+    match r' with
+    | EvalResult.Success sm => f sm env'
+    | EvalResult.Return v => (EvalResult.Return v, env')
+    | EvalResult.Exitting target => (EvalResult.Exitting target, env')
+    | EvalResult.TypeError msg => (EvalResult.TypeError msg, env')
+    | EvalResult.VerficationError et msg => (EvalResult.VerficationError et msg, env')
+
+def withResult {u: Type} (r : EvalResult u) : Eval u :=
+  fun env => (r, env)
+
+def evalOpWithoutDynamic (op : Operation) (args : List TypedValue) : Except (EvalResult TypedValue) TypedValue :=
+  let argTypes := args.map (fun a => a.ty)
+  match args with
+  | [arg1, arg2] =>
+    match op with
+    | Operation.Add =>
+        match argTypes with
+        | [HighType.TInt, HighType.TInt] => Except.ok <| TypedValue.mk (Value.VInt (arg1.val.asInt! + arg2.val.asInt!)) HighType.TInt
+        | [HighType.TFloat64, HighType.TFloat64] => Except.ok <| TypedValue.mk (Value.VFloat64 (arg1.val.asFloat64! + arg2.val.asFloat64!)) HighType.TFloat64
+        -- TOOD add other types
+        | _ => Except.error <| EvalResult.TypeError "Invalid types for Add"
+
+    | Operation.Eq =>
+      match argTypes with
+      | [HighType.TInt, HighType.TInt] => Except.ok <| { val := Value.VBool (arg1.val.asInt! == arg2.val.asInt!), ty := HighType.TBool }
+      | [HighType.TBool, HighType.TBool] => Except.ok <| { val := Value.VBool (arg1.val.asBool! == arg2.val.asBool!), ty := HighType.TBool }
+      | _ => Except.error <| EvalResult.TypeError "Invalid types for Eq"
+    | _ => Except.error <| EvalResult.TypeError "Operation not implemented"
+  | _ => Except.error <| EvalResult.TypeError s!"No operator with {args.length} arguments"
+
+def evalOp (op : Operation) (args : List TypedValue) : Except (EvalResult TypedValue) TypedValue :=
+  if (args.all fun a => a.ty.isDynamic) then
+    match evalOpWithoutDynamic op (args.map fun a => a.val.asBoxed!) with
+      | Except.ok v => Except.ok v
+      | Except.error (EvalResult.TypeError msg) =>
+          Except.error (EvalResult.VerficationError VerificationErrorType.PreconditionFailed msg)
+      | Except.error e => Except.error e
+  else
+    evalOpWithoutDynamic op args
+
+partial def eval (expr : StmtExpr) : Eval TypedValue :=
+  match expr with
+-- Expressions
+  | StmtExpr.LiteralBool b => pure <| TypedValue.mk (Value.VBool b) HighType.TBool
+  | StmtExpr.LiteralInt i => pure <| TypedValue.mk (Value.VInt i) HighType.TInt
+  | StmtExpr.Identifier name => getLocal name
+
+  | StmtExpr.IfThenElse condExpr thenBranch elseBranch => do
+    let cond <- eval condExpr
+    if (cond.ty.isBool) then
+      withResult <| EvalResult.TypeError "Condition must be boolean"
+    else
+      if cond.val.asBool! then eval thenBranch else
+        match elseBranch with
+        | some elseStmt => eval elseStmt
+        | none => pure voidTv
+
+  | StmtExpr.PrimitiveOp op args => do
+    let evalArgs ← args.mapM (fun arg => eval arg)
+    match evalOp op evalArgs with
+    | Except.ok val => pure val
+    | Except.error msg => withResult msg
+  | StmtExpr.StaticInvocation callee argumentsExprs => do
+    let env ← getEnv
+    match env.statics.get? callee with
+      | none => withResult <| EvalResult.TypeError s!"Undefined static method: {callee}"
+      | some callable => do
+        if callable.inputs.length != argumentsExprs.length then
+          withResult <| (EvalResult.TypeError s!"Static invocation of {callee} with wrong number of arguments")
+        else
+          let arguments ← argumentsExprs.mapM (fun arg => eval arg)
+          let mod ← match callable.purity with
+            | Purity.Impure modifies => eval modifies
+            | Purity.Pure reads => panic! "not implemented" -- pure { val := [], ty := }
+          let env ← getEnv
+          setEnv { env with heap := env.heap  } -- TODO: apply mod
+
+          pushStack
+          arguments.zip callable.inputs |>.forM (fun (arg, param) =>
+              if param.type != arg.ty then
+                withResult <| EvalResult.TypeError s!"Static invocation of {callee} with wrong type for argument {param.name}"
+              else
+                setLocal param.name arg
+            )
+          let precondition ← eval callable.precondition
+          assertBool precondition
+          -- TODO, handle decreases
+
+          let result: TypedValue ← match callable.body with
+            | Body.Transparent bodyExpr => do
+              let transparantResult ← eval bodyExpr
+              if transparantResult.ty != callable.output then
+                withResult <| EvalResult.TypeError s!"Static invocation of {callee} with wrong return type"
+              else
+                pure transparantResult
+            | Body.Opaque (postcondition: StmtExpr) _ => panic! "not implemented: opaque body"
+            | Body.Abstract (postcondition: StmtExpr) => panic! "not implemented: opaque body"
+          popStack
+          pure result
+
+-- Statements
+  | StmtExpr.Block stmts label => evalBlock label stmts
+
+-- Support locals
+  | StmtExpr.LocalVariable name _ (some init) => do
+      let value ← eval init
+      setLocal name value
+      return voidTv
+  | StmtExpr.LocalVariable name type none => do
+    setLocal name (TypedValue.mk Value.VUnknown type)
+    return voidTv
+  | StmtExpr.Assign (StmtExpr.Identifier localName) valueExpr => do
+    let value ← eval valueExpr
+    let oldTypedValue ← getLocal localName
+    setLocal localName (TypedValue.mk value.val oldTypedValue.ty)
+    pure voidTv
+-- Jumps
+  | StmtExpr.Return (some valExpr) => do
+    let tv ← eval valExpr
+    withResult (EvalResult.Return tv.val)
+  | StmtExpr.Return none => fun env => (EvalResult.Success { val := Value.VVoid, ty := env.returnType }, env)
+  | StmtExpr.While _ none _ _  => withResult <| EvalResult.TypeError "While invariant was not derived"
+  | StmtExpr.While _ _ none _  => withResult <| EvalResult.TypeError "While decreases was not derived"
+  | StmtExpr.While condExpr (some invariantExpr) (some decreasedExpr) bodyExpr => do
+    let rec loop : Eval TypedValue := do
+      let cond ← eval condExpr
+      if (cond.ty.isBool) then
+        withResult <| EvalResult.TypeError "Condition must be boolean"
+      else if cond.val.asBool! then
+        let invariant ← eval invariantExpr
+        if (invariant.ty.isBool) then
+          withResult <| EvalResult.TypeError "Invariant must be boolean"
+        else if (!invariant.val.asBool!) then
+          withResult <| EvalResult.VerficationError VerificationErrorType.InvariantFailed "While invariant does not hold"
+        else
+        -- TODO handle decreases
+          fun env => match eval bodyExpr env with
+            | (EvalResult.Success _, env') => loop env'
+            | other => other
+      else
+        pure voidTv
+    loop
+  | StmtExpr.Exit target => withResult <| EvalResult.Exitting target
+
+-- Support non-heap objects
+  | StmtExpr.PureFieldUpdate _ _ _ => panic! "not implemented: PureFieldUpdate"
+  | KnownFieldSelect _ _ => panic! "not implemented: StaticFieldSelect"
+
+-- Support heap objects
+  | StmtExpr.Assign (KnownFieldSelect objExpr fieldName) valueExpr =>
+    panic! "not implemented"
+  -- do
+  --     let objTv ← eval objExpr
+  --     match objTv.ty with
+  --     | HighType.UserDefined targetName => ()
+  --     if (objTv.ty != HighType.) then
+  --       return EvalResult.TypeError "Target object must be of type Dynamic"
+  --     match objTv.typ with
+  --     | EvalResult.Success { val := Value.VObject type fields, ty := _ } env'' =>
+  --       let newFields := fields.insertNew fieldName tv.val
+  --       let newObj := Value.VObject type newFields
+  --       EvalResult.Success voidTv env''.insertNew "_temp" (TypedValue.mk newObj HighType.Dynamic) -- TODO update variable holding the object
+  --     | EvalResult.Success _ _ => EvalResult.TypeError "Target is not an object"
+  --     | result => result
+  --    | _ => EvalResult.TypeError "Invalid assignment target"
+  | StmtExpr.Assign (StmtExpr.DynamicFieldAccess objExpr fieldName) valueExpr => panic! "not implemented"
+  | StmtExpr.Assign _ valueExpr => withResult <| EvalResult.TypeError "Invalid assignment target"
+
+-- Instance related
+  | StmtExpr.This => panic! "not implemented: This"
+  | StmtExpr.IsType _ _ _ => panic! "not implemented: IsType"
+  | StmtExpr.InstanceInvocation _ _ _ => panic! "not implemented: InstanceInvocation"
+
+-- Dynamic
+  | StmtExpr.Closure _ => panic! "not implemented: Closure"
+  | StmtExpr.DynamicInvocation _ _ => panic! "not implemented: DynamicInvocation"
+  | StmtExpr.DynamicFieldAccess _ _ => panic! "not implemented: DynamicFieldAccess"
+  | StmtExpr.DynamicFieldUpdate _ _ _ => panic! "not implemented: DynamicFieldUpdate"
+
+-- Verification statements
+  | StmtExpr.Assert condExpr => do
+    let cond ← eval condExpr
+    if cond.ty.isBool then
+      withResult <| EvalResult.TypeError "Condition must be boolean"
+    else if cond.val.asBool! then
+      pure voidTv
+    else
+      withResult <| EvalResult.VerficationError VerificationErrorType.PreconditionFailed "Assertion failed"
+  | StmtExpr.Assume _ => panic! "not implemented: Assume"
+  | StmtExpr.ProveBy _ _ => panic! "not implemented: ProveBy"
+  | StmtExpr.Assigned _ => panic! "not implemented: Assigned"
+
+-- Heap verification statements
+  | StmtExpr.Old _ => panic! "not implemented: Old"
+  | StmtExpr.Fresh _ => panic! "not implemented: Fresh"
+
+-- Construction
+  | StmtExpr.Create _ => panic! "not implemented: Create"
+  | StmtExpr.Complete _ => panic! "not implemented: Complete"
+
+-- Used for incomplete code during development
+  | StmtExpr.Hole => pure <| TypedValue.mk Value.VUnknown HighType.Dynamic
+  | _ => panic! "not implemented"
+
+
+where
+  evalBlock (labelOption: Option Identifier) (stmts : List StmtExpr) : Eval TypedValue :=
+    match stmts with
+    | [] => pure <| TypedValue.mk Value.VVoid HighType.TVoid
+    | stmt :: rest => fun env => match eval stmt env with
+      | (EvalResult.Exitting target, env') =>
+        let targetsMe := some target == labelOption
+        if targetsMe then
+          (EvalResult.Success voidTv, env')
+        else
+          evalBlock labelOption rest env'
+      | (EvalResult.Success _, env') => evalBlock labelOption rest env'
+      | other => other
+
+end HighLevel