diff --git a/.gitignore b/.gitignore
index 8028b846d..cd8092786 100644
--- a/.gitignore
+++ b/.gitignore
@@ -73,3 +73,4 @@ UPDATES-FOR-CHANGELOG.org
 docs/md/
 _docs
 docs/**/*.md
+**/html/*
diff --git a/examples/milestone/ValidityPredicates/Anoma/Base.mjuvix b/examples/milestone/ValidityPredicates/Anoma/Base.mjuvix
index 1c6f65892..84b7de91c 100644
--- a/examples/milestone/ValidityPredicates/Anoma/Base.mjuvix
+++ b/examples/milestone/ValidityPredicates/Anoma/Base.mjuvix
@@ -4,25 +4,60 @@ foreign ghc {
   import Anoma.Base
 };
 
+foreign c {
+  int readPre(const char *key) {
+      if (strcmp("change1-key", key)) {
+          return 100;
+      \} else if (strcmp("change2-key", key)) {
+          return 90;
+      \} else {
+          return -1;
+      \}
+  \}
+
+  int readPost(const char *key) {
+      if (strcmp("change1-key", key)) {
+          return 90;
+      \} else if (strcmp("change2-key", key)) {
+          return 100;
+      \} else {
+          return -1;
+      \}
+  \}
+
+  char* isBalanceKey(const char* s1, const char* s2) {
+      return "owner-address";
+  \}
+};
+
 import Prelude;
 open Prelude;
 
+from-int : Int → Maybe Int;
+from-int i ≔ if (i < 0) nothing (just i);
+
+from-string : String → Maybe String;
+from-string s ≔ if (s ==String "") nothing (just s);
+
 --------------------------------------------------------------------------------
 -- Anoma
 --------------------------------------------------------------------------------
 
 axiom readPre : String → Int;
 compile readPre {
+  c ↦ "readPre";
   ghc ↦ "readPre";
 };
 
 axiom readPost : String → Int;
 compile readPost {
+  c ↦ "readPost";
   ghc ↦ "readPost";
 };
 
 axiom isBalanceKey : String → String → String;
 compile isBalanceKey {
+  c ↦ "isBalanceKey";
   ghc ↦ "isBalanceKey";
 };
 
@@ -36,6 +71,6 @@ is-balance-key : String → String → Maybe String;
 is-balance-key token key ≔ from-string (isBalanceKey token key);
 
 unwrap-default : Maybe Int → Int;
-unwrap-default o ≔ maybe-int 0 o;
+unwrap-default ≔ maybe 0 id;
 
 end;
diff --git a/examples/milestone/ValidityPredicates/Data/Bool.mjuvix b/examples/milestone/ValidityPredicates/Data/Bool.mjuvix
index 4f9cbffa9..77701e45c 100644
--- a/examples/milestone/ValidityPredicates/Data/Bool.mjuvix
+++ b/examples/milestone/ValidityPredicates/Data/Bool.mjuvix
@@ -19,9 +19,9 @@ infixr 3 &&;
 && false _ ≔ false;
 && true a ≔ a;
 
-if : (A : Type) → Bool → A → A → A;
-if _ true a _ ≔ a;
-if _ false _ b ≔ b;
+if : {A : Type} → Bool → A → A → A;
+if true a _ ≔ a;
+if false _ b ≔ b;
 
 --------------------------------------------------------------------------------
 -- Backend Booleans
@@ -29,28 +29,38 @@ if _ false _ b ≔ b;
 
 axiom BackendBool : Type;
 compile BackendBool {
+  c ↦ "bool";
   ghc ↦ "Bool";
 };
 
 axiom backend-true : BackendBool;
 compile backend-true {
+  c ↦ "true";
   ghc ↦ "True";
 };
 
 axiom backend-false : BackendBool;
 compile backend-false {
+  c ↦ "false";
   ghc ↦ "False";
 };
 
-
 foreign ghc {
   bool :: Bool -> a -> a -> a
   bool True x _ = x
   bool False _ y = y
 };
 
+foreign c {
+  void* boolInd(bool b, void* a1, void* a2) {
+    return b ? a1 : a2;
+  \}
+};
+
+
 axiom bool : BackendBool → Bool → Bool → Bool;
 compile bool {
+  c ↦ "boolInd";
   ghc ↦ "bool";
 };
 
diff --git a/examples/milestone/ValidityPredicates/Data/Int.mjuvix b/examples/milestone/ValidityPredicates/Data/Int.mjuvix
index 291803dc9..30c002551 100644
--- a/examples/milestone/ValidityPredicates/Data/Int.mjuvix
+++ b/examples/milestone/ValidityPredicates/Data/Int.mjuvix
@@ -3,18 +3,34 @@ module Data.Int;
 import Data.Bool;
 open Data.Bool;
 
---------------------------------------------------------------------------------
--- Integers
---------------------------------------------------------------------------------
-
 axiom Int : Type;
 compile Int {
+  c ↦ "int";
   ghc ↦ "Int";
 };
 
+foreign c {
+   bool lessThan(int l, int r) {
+     return l < r;
+   \}
+
+   bool eqInt(int l, int r) {
+     return l == r;
+   \}
+
+   int plus(int l, int r) {
+     return l + r;
+   \}
+
+   int minus(int l, int r) {
+     return l - r;
+   \}
+};
+
 infix 4 <';
 axiom <' : Int → Int → BackendBool;
 compile <' {
+  c ↦ "lessThan";
   ghc ↦ "(<)";
 };
 
@@ -24,6 +40,7 @@ infix 4 <;
 
 axiom eqInt : Int → Int → BackendBool;
 compile eqInt {
+  c ↦ "eqInt";
   ghc ↦ "(==)";
 };
 
@@ -34,12 +51,14 @@ infix 4 ==Int;
 infixl 6 -;
 axiom - : Int -> Int -> Int;
 compile - {
+  c ↦ "minus";
   ghc ↦ "(-)";
 };
 
 infixl 6 +;
 axiom + : Int -> Int -> Int;
 compile + {
+  c ↦ "plus";
   ghc ↦ "(+)";
 };
 
diff --git a/examples/milestone/ValidityPredicates/Data/List.mjuvix b/examples/milestone/ValidityPredicates/Data/List.mjuvix
index 49909bf2f..0cb615658 100644
--- a/examples/milestone/ValidityPredicates/Data/List.mjuvix
+++ b/examples/milestone/ValidityPredicates/Data/List.mjuvix
@@ -3,24 +3,18 @@ module Data.List;
 import Data.Bool;
 open Data.Bool;
 
-import Data.String;
-open Data.String;
-
---------------------------------------------------------------------------------
--- Lists
---------------------------------------------------------------------------------
-
+infixr 5 ∷;
 inductive List (A : Type) {
   nil : List A;
-  cons : A → List A → List A;
+  ∷ : A → List A → List A;
 };
 
-elem : (A : Type) → (A → A → Bool) → A → List A → Bool;
-elem _ _ _ nil ≔ false;
-elem A eq s (cons x xs) ≔ eq s x || elem _ eq s xs;
+elem : {A : Type} → (A → A → Bool) → A → List A → Bool;
+elem _ _ nil ≔ false;
+elem eq s (x ∷ xs) ≔ eq s x || elem eq s xs;
 
-foldl : (A : Type) → (B : Type) → (B → A → B) → B → List A → B;
-foldl _ _ f z nil ≔ z;
-foldl A B f z (cons h hs) ≔ foldl _ _ f (f z h) hs;
+foldl : {A : Type} → {B : Type} → (B → A → B) → B → List A → B;
+foldl f z nil ≔ z;
+foldl f z (h ∷ hs) ≔ foldl f (f z h) hs;
 
 end;
diff --git a/examples/milestone/ValidityPredicates/Data/Maybe.mjuvix b/examples/milestone/ValidityPredicates/Data/Maybe.mjuvix
index dd6eb2b95..6c6f0736a 100644
--- a/examples/milestone/ValidityPredicates/Data/Maybe.mjuvix
+++ b/examples/milestone/ValidityPredicates/Data/Maybe.mjuvix
@@ -1,16 +1,21 @@
 module Data.Maybe;
 
---------------------------------------------------------------------------------
--- Maybe
---------------------------------------------------------------------------------
+import Data.Int;
+open Data.Int;
+
+import Data.Bool;
+open Data.Bool;
 
 inductive Maybe (A : Type) {
  nothing : Maybe A;
  just : A → Maybe A;
 };
 
-maybe : (A : Type) → (B : Type) → B → (A → B) → Maybe A → B;
-maybe _ _ b _ nothing ≔ b;
-maybe _ _ _ f (just x) ≔ f x;
+-- from-int : Int → Maybe Int;
+-- from-int i ≔ if (i < 0) nothing (just i);
+
+maybe : {A : Type} → {B : Type} → B → (A → B) → Maybe A → B;
+maybe b _ nothing ≔ b;
+maybe _ f (just x) ≔ f x;
 
 end;
diff --git a/examples/milestone/ValidityPredicates/Data/Pair.mjuvix b/examples/milestone/ValidityPredicates/Data/Pair.mjuvix
index 39234a602..3bd4ceb69 100644
--- a/examples/milestone/ValidityPredicates/Data/Pair.mjuvix
+++ b/examples/milestone/ValidityPredicates/Data/Pair.mjuvix
@@ -1,12 +1,9 @@
 module Data.Pair;
 
-
---------------------------------------------------------------------------------
--- Pair
---------------------------------------------------------------------------------
-
-inductive Pair (A : Type) (B : Type) {
-  mkPair : A → B → Pair A B;
+infixr 4 ,;
+infixr 2 ×;
+inductive × (A : Type) (B : Type) {
+  , : A → B → A × B;
 };
 
 end;
diff --git a/examples/milestone/ValidityPredicates/Data/String.mjuvix b/examples/milestone/ValidityPredicates/Data/String.mjuvix
index 751907a71..ad0796120 100644
--- a/examples/milestone/ValidityPredicates/Data/String.mjuvix
+++ b/examples/milestone/ValidityPredicates/Data/String.mjuvix
@@ -3,17 +3,21 @@ module Data.String;
 import Data.Bool;
 open Data.Bool;
 
---------------------------------------------------------------------------------
--- Strings
---------------------------------------------------------------------------------
-
 axiom String : Type;
 compile String {
+  c ↦ "char*";
   ghc ↦ "[Char]";
 };
 
+foreign c {
+  bool eqString(char* l, char* r) {
+    return strcmp(l, r) == 0;
+  \}
+};
+
 axiom eqString : String → String → BackendBool;
 compile eqString  {
+  c ↦ "eqString";
   ghc ↦ "(==)";
 };
 
diff --git a/examples/milestone/ValidityPredicates/FungibleToken.mjuvix b/examples/milestone/ValidityPredicates/FungibleToken.mjuvix
deleted file mode 100644
index 705a748ec..000000000
--- a/examples/milestone/ValidityPredicates/FungibleToken.mjuvix
+++ /dev/null
@@ -1,51 +0,0 @@
-module FungibleToken;
-
-import Anoma.Base;
-open Anoma.Base;
-
-import Prelude;
-open Prelude;
-
---------------------------------------------------------------------------------
--- Misc
---------------------------------------------------------------------------------
-
-pair-from-optionString : (String → Pair Int Bool) → Maybe String → Pair Int Bool;
-pair-from-optionString ≔ maybe String (Pair Int Bool) (mkPair Int Bool 0 false);
-
-check-result : Pair Int Bool → Bool;
-check-result (mkPair change all-checked) ≔ (change ==Int 0) && all-checked;
-
---------------------------------------------------------------------------------
--- Validity Predicate
---------------------------------------------------------------------------------
-
-change-from-key : String → Int;
-change-from-key key ≔ unwrap-default (read-post key)
-                    - unwrap-default (read-pre key);
-
-check-vp : List String → String → Int → String → Pair Int Bool;
-check-vp verifiers key change owner ≔
-    if _
-      -- make sure the spender approved the transaction
-      (change-from-key key < 0)
-        (mkPair _ _ (change + (change-from-key key))
-                (elem _ (==String) owner verifiers))
-        (mkPair _ _ (change + (change-from-key key)) true);
-
-check-keys : String → List String → Pair Int Bool → String → Pair Int Bool;
-check-keys token verifiers (mkPair change is-success) key ≔
-    if _
-        is-success
-        (pair-from-optionString (check-vp verifiers key change)
-           (is-balance-key token key))
-        (mkPair _ _ 0 false);
-
-vp : String → List String → List String → Bool;
-vp token keys-changed verifiers ≔
-    check-result
-        (foldl _ _
-            (check-keys token verifiers)
-            (mkPair _ _ 0 true)
-            keys-changed);
-end;
diff --git a/examples/milestone/ValidityPredicates/Prelude.mjuvix b/examples/milestone/ValidityPredicates/Prelude.mjuvix
index 183cf3075..ab66ee0ca 100644
--- a/examples/milestone/ValidityPredicates/Prelude.mjuvix
+++ b/examples/milestone/ValidityPredicates/Prelude.mjuvix
@@ -2,19 +2,19 @@ module Prelude;
 
 import Data.Bool;
 import Data.Int;
+import Data.String;
 import Data.List;
 import Data.Maybe;
 import Data.Pair;
-import Data.String;
 import System.IO;
 
-open Data.Bool;
-open Data.Int;
-open Data.List;
-open Data.Maybe;
-open Data.Pair;
-open Data.String;
-open System.IO;
+open Data.Bool public;
+open Data.Int public;
+open Data.String public;
+open Data.List public;
+open Data.Maybe public;
+open Data.Pair public;
+open System.IO public;
 
 --------------------------------------------------------------------------------
 -- Functions
@@ -23,7 +23,7 @@ open System.IO;
 const : (A : Type) → (B : Type) → A → B → A;
 const _ _ a _ ≔ a;
 
-id : (A : Type) → A → A;
-id _ a ≔ a;
+id : {A : Type} → A → A;
+id a ≔ a;
 
 end;
diff --git a/examples/milestone/ValidityPredicates/SimpleFungibleToken.mjuvix b/examples/milestone/ValidityPredicates/SimpleFungibleToken.mjuvix
new file mode 100644
index 000000000..adfe1b728
--- /dev/null
+++ b/examples/milestone/ValidityPredicates/SimpleFungibleToken.mjuvix
@@ -0,0 +1,48 @@
+module SimpleFungibleToken;
+
+import Anoma.Base;
+open Anoma.Base;
+
+import Prelude;
+open Prelude;
+
+--------------------------------------------------------------------------------
+-- Misc
+--------------------------------------------------------------------------------
+
+pair-from-optionString : (String → Int × Bool) → Maybe String → Int × Bool;
+pair-from-optionString ≔ maybe (0 , false);
+
+--------------------------------------------------------------------------------
+-- Validity Predicate
+--------------------------------------------------------------------------------
+
+change-from-key : String → Int;
+change-from-key key ≔ unwrap-default (read-post key) - unwrap-default (read-pre key);
+
+check-vp : List String → String → Int → String → Int × Bool;
+check-vp verifiers key change owner ≔
+    if
+        (change-from-key key < 0)
+        -- make sure the spender approved the transaction
+        (change + (change-from-key key), elem (==String) owner verifiers)
+        (change + (change-from-key key),  true);
+
+check-keys : String → List String → Int × Bool → String → Int × Bool;
+check-keys token verifiers (change , is-success) key ≔
+    if
+        is-success
+        (pair-from-optionString (check-vp verifiers key change) (is-balance-key token key))
+        (0 , false);
+
+check-result : Int × Bool → Bool;
+check-result (change , all-checked) ≔ (change ==Int 0) && all-checked;
+
+vp : String → List String → List String → Bool;
+vp token keys-changed verifiers ≔
+    check-result
+        (foldl
+            (check-keys token verifiers)
+            (0 , true)
+            keys-changed);
+end;
diff --git a/examples/milestone/ValidityPredicates/System/IO.mjuvix b/examples/milestone/ValidityPredicates/System/IO.mjuvix
index e1fd9852e..3a839f97d 100644
--- a/examples/milestone/ValidityPredicates/System/IO.mjuvix
+++ b/examples/milestone/ValidityPredicates/System/IO.mjuvix
@@ -1,27 +1,39 @@
 module System.IO;
 
---------------------------------------------------------------------------------
--- Actions
---------------------------------------------------------------------------------
+import Data.String;
+open Data.String;
+
+import Data.Bool;
+open Data.Bool;
 
 axiom Action : Type;
 compile Action {
- ghc ↦ "IO ()";
+  c ↦ "int";
+  ghc ↦ "IO ()";
 };
 
 axiom putStr : String → Action;
 compile putStr {
+  c ↦ "putStr";
   ghc ↦ "putStr";
 };
 
 axiom putStrLn : String → Action;
 compile putStrLn {
+  c ↦ "putStrLn";
   ghc ↦ "putStrLn";
 };
 
+foreign c {
+  int sequence(int a, int b) {
+    return a + b;
+  \}
+};
+
 infixl 1 >>;
 axiom >> : Action → Action → Action;
 compile >> {
+  c ↦ "sequence";
   ghc ↦ "(>>)";
 };
 
diff --git a/examples/milestone/ValidityPredicates/Tests.mjuvix b/examples/milestone/ValidityPredicates/Tests.mjuvix
index 39282fa74..eff7be565 100644
--- a/examples/milestone/ValidityPredicates/Tests.mjuvix
+++ b/examples/milestone/ValidityPredicates/Tests.mjuvix
@@ -23,15 +23,14 @@ change2-key : String;
 change2-key ≔ "change2-key";
 
 verifiers : List String;
-verifiers ≔ cons String owner-address (nil String);
+verifiers ≔ owner-address ∷ nil;
 
 keys-changed : List String;
-keys-changed ≔ cons String change1-key (cons String change2-key (nil String));
+keys-changed ≔ change1-key ∷ change2-key ∷ nil;
 
 main : Action;
 main ≔
     (putStr "VP Status: ")
     >> (putStrLn (show-result (vp token keys-changed verifiers)));
-end;
 
 end;
diff --git a/examples/milestone/ValidityPredicates/minijuvix.yaml b/examples/milestone/ValidityPredicates/minijuvix.yaml
new file mode 100644
index 000000000..e69de29bb
diff --git a/package.yaml b/package.yaml
index b20958c02..9e83cb791 100644
--- a/package.yaml
+++ b/package.yaml
@@ -14,6 +14,7 @@ github:          heliaxdev/minijuvix
 
 extra-source-files:
 - README.org
+- assets/*
 
 dependencies:
 - ansi-terminal == 0.11.*