diff --git a/src/bin/expect_tests/contract_tests.ml b/src/bin/expect_tests/contract_tests.ml
index b78762e37..2dbe3ad34 100644
--- a/src/bin/expect_tests/contract_tests.ml
+++ b/src/bin/expect_tests/contract_tests.ml
@@ -5,16 +5,16 @@ let contract basename =
 
 let%expect_test _ =
   run_ligo_good [ "measure-contract" ; contract "coase.ligo" ; "main" ] ;
-  [%expect {| 3098 bytes |}] ;
+  [%expect {| 2068 bytes |}] ;
 
   run_ligo_good [ "measure-contract" ; contract "multisig.ligo" ; "main" ] ;
-  [%expect {| 1367 bytes |}] ;
+  [%expect {| 1093 bytes |}] ;
 
   run_ligo_good [ "measure-contract" ; contract "multisig-v2.ligo" ; "main" ] ;
-  [%expect {| 861 bytes |}] ;
+  [%expect {| 627 bytes |}] ;
 
   run_ligo_good [ "measure-contract" ; contract "vote.mligo" ; "main" ] ;
-  [%expect {| 1344 bytes |}] ;
+  [%expect {| 714 bytes |}] ;
 
   ()
 
@@ -28,16 +28,191 @@ let%expect_test _ =
         (pair (pair (map %card_patterns nat (pair (mutez %coefficient) (nat %quantity)))
                     (map %cards nat (pair (address %card_owner) (nat %card_pattern))))
               (nat %next_id)) ;
-      code { LAMBDA
-               (pair (pair (nat %card_to_transfer) (address %destination))
-                     (pair (pair (map %card_patterns nat (pair (mutez %coefficient) (nat %quantity)))
-                                 (map %cards nat (pair (address %card_owner) (nat %card_pattern))))
-                           (nat %next_id)))
-               (pair (list operation)
-                     (pair (pair (map %card_patterns nat (pair (mutez %coefficient) (nat %quantity)))
-                                 (map %cards nat (pair (address %card_owner) (nat %card_pattern))))
-                           (nat %next_id)))
+      code { DUP ;
+             CDR ;
+             DIP { DUP } ;
+             SWAP ;
+             CAR ;
+             IF_LEFT
                { DUP ;
+                 IF_LEFT
+                   { DUP ;
+                     DIP { DIP 2 { DUP } ; DIG 2 } ;
+                     PAIR ;
+                     DUP ;
+                     CAR ;
+                     DIP { DUP } ;
+                     SWAP ;
+                     CDR ;
+                     DIP { DUP } ;
+                     SWAP ;
+                     DIP { DUP ; CAR ; CAR } ;
+                     GET ;
+                     IF_NONE { PUSH string "GET_FORCE" ; FAILWITH } {} ;
+                     DUP ;
+                     CAR ;
+                     DIP { DUP ; CDR ; PUSH nat 1 ; ADD } ;
+                     MUL ;
+                     DUP ;
+                     AMOUNT ;
+                     SWAP ;
+                     COMPARE ;
+                     GT ;
+                     IF { PUSH string "Not enough money" ; FAILWITH } { PUSH unit Unit } ;
+                     DROP ;
+                     NIL operation ;
+                     DIP 2 { DUP } ;
+                     DIG 2 ;
+                     CDR ;
+                     PUSH nat 1 ;
+                     ADD ;
+                     DIP { DIP 2 { DUP } ; DIG 2 ; CAR } ;
+                     SWAP ;
+                     PAIR ;
+                     DIP 3 { DROP } ;
+                     DUG 2 ;
+                     DIP 3 { DUP } ;
+                     DIG 3 ;
+                     CAR ;
+                     CAR ;
+                     DIP 5 { DUP } ;
+                     DIG 5 ;
+                     DIP { DIP 3 { DUP } ; DIG 3 ; SOME ; DIP { DUP } } ;
+                     UPDATE ;
+                     DIP { DROP } ;
+                     DUP ;
+                     DIP { DIP 4 { DUP } ; DIG 4 ; DUP ; CDR ; SWAP ; CAR ; CDR } ;
+                     PAIR ;
+                     PAIR ;
+                     DIP 5 { DROP } ;
+                     DUG 4 ;
+                     DIP 4 { DUP } ;
+                     DIG 4 ;
+                     CAR ;
+                     CDR ;
+                     DIP 5 { DUP } ;
+                     DIG 5 ;
+                     CDR ;
+                     DIP { DIP 6 { DUP } ; DIG 6 ; SOURCE ; PAIR ; SOME ; DIP { DUP } } ;
+                     UPDATE ;
+                     DIP { DROP } ;
+                     DUP ;
+                     DIP { DIP 5 { DUP } ; DIG 5 ; DUP ; CDR ; SWAP ; CAR ; CAR } ;
+                     SWAP ;
+                     PAIR ;
+                     PAIR ;
+                     DIP 6 { DROP } ;
+                     DUG 5 ;
+                     DIP 5 { DUP } ;
+                     DIG 5 ;
+                     CDR ;
+                     PUSH nat 1 ;
+                     ADD ;
+                     DIP { DIP 5 { DUP } ; DIG 5 ; CAR } ;
+                     SWAP ;
+                     PAIR ;
+                     DIP 6 { DROP } ;
+                     DUG 5 ;
+                     DIP 2 { DUP } ;
+                     DIG 2 ;
+                     DIP { DIP 5 { DUP } ; DIG 5 } ;
+                     PAIR ;
+                     DIP { DROP 9 } }
+                   { DUP ;
+                     DIP { DIP 2 { DUP } ; DIG 2 } ;
+                     PAIR ;
+                     DUP ;
+                     CAR ;
+                     DIP { DUP } ;
+                     SWAP ;
+                     CDR ;
+                     DIP { DUP } ;
+                     SWAP ;
+                     DIP { DUP ; CAR ; CDR } ;
+                     GET ;
+                     IF_NONE { PUSH string "GET_FORCE" ; FAILWITH } {} ;
+                     DUP ;
+                     CAR ;
+                     SOURCE ;
+                     SWAP ;
+                     COMPARE ;
+                     NEQ ;
+                     IF { PUSH string "This card doesn't belong to you" ; FAILWITH }
+                        { PUSH unit Unit } ;
+                     DROP ;
+                     DUP ;
+                     CDR ;
+                     DIP { DIP { DUP } ; SWAP ; CAR ; CAR } ;
+                     GET ;
+                     IF_NONE { PUSH string "GET_FORCE" ; FAILWITH } {} ;
+                     DUP ;
+                     CDR ;
+                     PUSH nat 1 ;
+                     SWAP ;
+                     SUB ;
+                     ABS ;
+                     DIP { DUP ; CAR } ;
+                     SWAP ;
+                     PAIR ;
+                     DIP { DROP } ;
+                     DIP 2 { DUP } ;
+                     DIG 2 ;
+                     CAR ;
+                     CAR ;
+                     DIP 2 { DUP } ;
+                     DIG 2 ;
+                     CDR ;
+                     DIP { DIP { DUP } ; SWAP ; SOME ; DIP { DUP } } ;
+                     UPDATE ;
+                     DIP { DROP } ;
+                     DUP ;
+                     DIP { DIP 3 { DUP } ; DIG 3 ; DUP ; CDR ; SWAP ; CAR ; CDR } ;
+                     PAIR ;
+                     PAIR ;
+                     DIP 4 { DROP } ;
+                     DUG 3 ;
+                     DIP 3 { DUP } ;
+                     DIG 3 ;
+                     CAR ;
+                     CDR ;
+                     DIP 5 { DUP } ;
+                     DIG 5 ;
+                     DIP { DUP ; NONE (pair (address %card_owner) (nat %card_pattern)) } ;
+                     UPDATE ;
+                     DIP { DROP } ;
+                     DUP ;
+                     DIP { DIP 4 { DUP } ; DIG 4 ; DUP ; CDR ; SWAP ; CAR ; CAR } ;
+                     SWAP ;
+                     PAIR ;
+                     PAIR ;
+                     DIP 5 { DROP } ;
+                     DUG 4 ;
+                     DIP 2 { DUP } ;
+                     DIG 2 ;
+                     CAR ;
+                     DIP { DIP 2 { DUP } ; DIG 2 ; CDR } ;
+                     MUL ;
+                     SOURCE ;
+                     CONTRACT unit ;
+                     IF_NONE { PUSH string "bad address for get_contract" ; FAILWITH } {} ;
+                     DIP { DUP } ;
+                     SWAP ;
+                     DIP { DUP } ;
+                     UNIT ;
+                     TRANSFER_TOKENS ;
+                     DUP ;
+                     NIL operation ;
+                     SWAP ;
+                     CONS ;
+                     DUP ;
+                     DIP { DIP 8 { DUP } ; DIG 8 } ;
+                     PAIR ;
+                     DIP { DROP 12 } } ;
+                 DIP { DROP } }
+               { DUP ;
+                 DIP { DIP { DUP } ; SWAP } ;
+                 PAIR ;
+                 DUP ;
                  CAR ;
                  DIP { DUP } ;
                  SWAP ;
@@ -81,229 +256,12 @@ let%expect_test _ =
                  PAIR ;
                  DIP 3 { DROP } ;
                  DUG 2 ;
+                 DIP 2 { DUP } ;
+                 DIG 2 ;
                  NIL operation ;
-                 DUP ;
-                 DIP { DIP 3 { DUP } ; DIG 3 } ;
                  PAIR ;
                  DIP { DROP 6 } } ;
-             LAMBDA
-               (pair nat
-                     (pair (pair (map %card_patterns nat (pair (mutez %coefficient) (nat %quantity)))
-                                 (map %cards nat (pair (address %card_owner) (nat %card_pattern))))
-                           (nat %next_id)))
-               (pair (list operation)
-                     (pair (pair (map %card_patterns nat (pair (mutez %coefficient) (nat %quantity)))
-                                 (map %cards nat (pair (address %card_owner) (nat %card_pattern))))
-                           (nat %next_id)))
-               { DUP ;
-                 CAR ;
-                 DIP { DUP } ;
-                 SWAP ;
-                 CDR ;
-                 DIP { DUP } ;
-                 SWAP ;
-                 DIP { DUP ; CAR ; CDR } ;
-                 GET ;
-                 IF_NONE { PUSH string "GET_FORCE" ; FAILWITH } {} ;
-                 DUP ;
-                 CAR ;
-                 SOURCE ;
-                 SWAP ;
-                 COMPARE ;
-                 NEQ ;
-                 IF { PUSH string "This card doesn't belong to you" ; FAILWITH }
-                    { PUSH unit Unit } ;
-                 DROP ;
-                 DUP ;
-                 CDR ;
-                 DIP { DIP { DUP } ; SWAP ; CAR ; CAR } ;
-                 GET ;
-                 IF_NONE { PUSH string "GET_FORCE" ; FAILWITH } {} ;
-                 DUP ;
-                 CDR ;
-                 PUSH nat 1 ;
-                 SWAP ;
-                 SUB ;
-                 ABS ;
-                 DIP { DUP ; CAR } ;
-                 SWAP ;
-                 PAIR ;
-                 DIP { DROP } ;
-                 DIP 2 { DUP } ;
-                 DIG 2 ;
-                 CAR ;
-                 CAR ;
-                 DIP 2 { DUP } ;
-                 DIG 2 ;
-                 CDR ;
-                 DIP { DIP { DUP } ; SWAP ; SOME ; DIP { DUP } } ;
-                 UPDATE ;
-                 DIP { DROP } ;
-                 DUP ;
-                 DIP { DIP 3 { DUP } ; DIG 3 ; DUP ; CDR ; SWAP ; CAR ; CDR } ;
-                 PAIR ;
-                 PAIR ;
-                 DIP 4 { DROP } ;
-                 DUG 3 ;
-                 DIP 3 { DUP } ;
-                 DIG 3 ;
-                 CAR ;
-                 CDR ;
-                 DIP 5 { DUP } ;
-                 DIG 5 ;
-                 DIP { DUP ; NONE (pair (address %card_owner) (nat %card_pattern)) } ;
-                 UPDATE ;
-                 DIP { DROP } ;
-                 DUP ;
-                 DIP { DIP 4 { DUP } ; DIG 4 ; DUP ; CDR ; SWAP ; CAR ; CAR } ;
-                 SWAP ;
-                 PAIR ;
-                 PAIR ;
-                 DIP 5 { DROP } ;
-                 DUG 4 ;
-                 DIP 2 { DUP } ;
-                 DIG 2 ;
-                 CAR ;
-                 DIP { DIP 2 { DUP } ; DIG 2 ; CDR } ;
-                 MUL ;
-                 SOURCE ;
-                 CONTRACT unit ;
-                 IF_NONE { PUSH string "bad address for get_contract" ; FAILWITH } {} ;
-                 DIP { DUP } ;
-                 SWAP ;
-                 DIP { DUP } ;
-                 UNIT ;
-                 TRANSFER_TOKENS ;
-                 DUP ;
-                 NIL operation ;
-                 SWAP ;
-                 CONS ;
-                 DUP ;
-                 DIP { DIP 8 { DUP } ; DIG 8 } ;
-                 PAIR ;
-                 DIP { DROP 11 } } ;
-             LAMBDA
-               (pair nat
-                     (pair (pair (map %card_patterns nat (pair (mutez %coefficient) (nat %quantity)))
-                                 (map %cards nat (pair (address %card_owner) (nat %card_pattern))))
-                           (nat %next_id)))
-               (pair (list operation)
-                     (pair (pair (map %card_patterns nat (pair (mutez %coefficient) (nat %quantity)))
-                                 (map %cards nat (pair (address %card_owner) (nat %card_pattern))))
-                           (nat %next_id)))
-               { DUP ;
-                 CAR ;
-                 DIP { DUP } ;
-                 SWAP ;
-                 CDR ;
-                 DIP { DUP } ;
-                 SWAP ;
-                 DIP { DUP ; CAR ; CAR } ;
-                 GET ;
-                 IF_NONE { PUSH string "GET_FORCE" ; FAILWITH } {} ;
-                 DUP ;
-                 CAR ;
-                 DIP { DUP ; CDR ; PUSH nat 1 ; ADD } ;
-                 MUL ;
-                 DUP ;
-                 AMOUNT ;
-                 SWAP ;
-                 COMPARE ;
-                 GT ;
-                 IF { PUSH string "Not enough money" ; FAILWITH } { PUSH unit Unit } ;
-                 DROP ;
-                 NIL operation ;
-                 DIP 2 { DUP } ;
-                 DIG 2 ;
-                 CDR ;
-                 PUSH nat 1 ;
-                 ADD ;
-                 DIP { DIP 2 { DUP } ; DIG 2 ; CAR } ;
-                 SWAP ;
-                 PAIR ;
-                 DIP 3 { DROP } ;
-                 DUG 2 ;
-                 DIP 3 { DUP } ;
-                 DIG 3 ;
-                 CAR ;
-                 CAR ;
-                 DIP 5 { DUP } ;
-                 DIG 5 ;
-                 DIP { DIP 3 { DUP } ; DIG 3 ; SOME ; DIP { DUP } } ;
-                 UPDATE ;
-                 DIP { DROP } ;
-                 DUP ;
-                 DIP { DIP 4 { DUP } ; DIG 4 ; DUP ; CDR ; SWAP ; CAR ; CDR } ;
-                 PAIR ;
-                 PAIR ;
-                 DIP 5 { DROP } ;
-                 DUG 4 ;
-                 DIP 4 { DUP } ;
-                 DIG 4 ;
-                 CAR ;
-                 CDR ;
-                 DIP 5 { DUP } ;
-                 DIG 5 ;
-                 CDR ;
-                 DIP { DIP 6 { DUP } ; DIG 6 ; SOURCE ; PAIR ; SOME ; DIP { DUP } } ;
-                 UPDATE ;
-                 DIP { DROP } ;
-                 DUP ;
-                 DIP { DIP 5 { DUP } ; DIG 5 ; DUP ; CDR ; SWAP ; CAR ; CAR } ;
-                 SWAP ;
-                 PAIR ;
-                 PAIR ;
-                 DIP 6 { DROP } ;
-                 DUG 5 ;
-                 DIP 5 { DUP } ;
-                 DIG 5 ;
-                 CDR ;
-                 PUSH nat 1 ;
-                 ADD ;
-                 DIP { DIP 5 { DUP } ; DIG 5 ; CAR } ;
-                 SWAP ;
-                 PAIR ;
-                 DIP 6 { DROP } ;
-                 DUG 5 ;
-                 DIP 2 { DUP } ;
-                 DIG 2 ;
-                 DIP { DIP 5 { DUP } ; DIG 5 } ;
-                 PAIR ;
-                 DIP { DROP 8 } } ;
-             DIP 3 { DUP } ;
-             DIG 3 ;
-             CAR ;
-             DIP 4 { DUP } ;
-             DIG 4 ;
-             CDR ;
-             DIP { DUP } ;
-             SWAP ;
-             IF_LEFT
-               { DUP ;
-                 IF_LEFT
-                   { DUP ;
-                     DUP ;
-                     DIP { DIP 3 { DUP } ; DIG 3 } ;
-                     PAIR ;
-                     DIP { DIP 5 { DUP } ; DIG 5 } ;
-                     EXEC ;
-                     DIP { DROP 2 } }
-                   { DUP ;
-                     DUP ;
-                     DIP { DIP 3 { DUP } ; DIG 3 } ;
-                     PAIR ;
-                     DIP { DIP 6 { DUP } ; DIG 6 } ;
-                     EXEC ;
-                     DIP { DROP 2 } } ;
-                 DIP { DROP } }
-               { DUP ;
-                 DUP ;
-                 DIP { DIP 2 { DUP } ; DIG 2 } ;
-                 PAIR ;
-                 DIP { DIP 6 { DUP } ; DIG 6 } ;
-                 EXEC ;
-                 DIP { DROP 2 } } ;
-             DIP { DROP 6 } } } |} ]
+             DIP { DROP 2 } } } |} ]
 
 let%expect_test _ =
   run_ligo_good [ "compile-contract" ; contract "multisig.ligo" ; "main" ] ;
@@ -314,139 +272,123 @@ let%expect_test _ =
       storage
         (pair (pair (list %auth key) (nat %counter)) (pair (string %id) (nat %threshold))) ;
       code { DUP ;
-             LAMBDA
-               (pair (pair (pair (nat %counter) (lambda %message unit (list operation)))
-                           (list %signatures (pair key_hash signature)))
-                     (pair (pair (list %auth key) (nat %counter)) (pair (string %id) (nat %threshold))))
-               (pair (list operation)
-                     (pair (pair (list %auth key) (nat %counter)) (pair (string %id) (nat %threshold))))
-               { DUP ;
-                 CAR ;
-                 DIP { DUP } ;
-                 SWAP ;
-                 CDR ;
-                 DIP { DUP } ;
-                 SWAP ;
-                 CAR ;
-                 CDR ;
-                 DIP 2 { DUP } ;
-                 DIG 2 ;
-                 CAR ;
-                 CAR ;
-                 DIP { DIP { DUP } ; SWAP ; CAR ; CDR } ;
-                 COMPARE ;
-                 NEQ ;
-                 IF { PUSH string "Counters does not match" ; FAILWITH }
-                    { DUP ;
-                      DIP { DIP 2 { DUP } ; DIG 2 ; CAR ; CAR } ;
-                      PAIR ;
-                      DIP { DIP { DUP } ; SWAP ; CDR ; CAR ; CHAIN_ID ; SWAP ; PAIR } ;
-                      PAIR ;
-                      PACK ;
-                      PUSH nat 0 ;
-                      DIP 3 { DUP } ;
-                      DIG 3 ;
-                      CAR ;
-                      CAR ;
-                      DIP 5 { DUP } ;
-                      DIG 5 ;
-                      CDR ;
-                      DIP { DUP ; DIP { DIP { DUP } ; SWAP } ; PAIR } ;
-                      ITER { SWAP ;
-                             PAIR ;
-                             DUP ;
-                             CAR ;
-                             DIP { DUP } ;
-                             SWAP ;
-                             CDR ;
-                             DIP { DUP } ;
-                             SWAP ;
-                             CAR ;
-                             IF_CONS
-                               { DIP { DUP } ;
-                                 SWAP ;
-                                 DIP { DIP 3 { DUP } ; DIG 3 ; CDR } ;
-                                 PAIR ;
-                                 DIP 4 { DROP } ;
-                                 DUG 3 ;
-                                 DIP 2 { DUP } ;
-                                 DIG 2 ;
-                                 CAR ;
-                                 DIP { DUP ; HASH_KEY } ;
-                                 COMPARE ;
-                                 EQ ;
-                                 IF { DUP ;
-                                      DIP { DIP 2 { DUP } ; DIG 2 ; CDR ; DIP { DIP 7 { DUP } ; DIG 7 } } ;
-                                      CHECK_SIGNATURE ;
-                                      IF { DIP 3 { DUP } ;
-                                           DIG 3 ;
-                                           CDR ;
-                                           PUSH nat 1 ;
-                                           ADD ;
-                                           DIP { DIP 3 { DUP } ; DIG 3 ; CAR } ;
-                                           SWAP ;
-                                           PAIR ;
-                                           DIP 4 { DROP } ;
-                                           DUG 3 ;
-                                           PUSH unit Unit }
-                                         { PUSH string "Invalid signature" ; FAILWITH } }
-                                    { PUSH unit Unit } ;
-                                 DIP { DROP 2 } }
-                               { PUSH unit Unit } ;
-                             DROP ;
-                             DIP { DUP } ;
-                             SWAP ;
-                             DIP { DROP 3 } } ;
-                      DUP ;
-                      CAR ;
-                      DIP { DIP { DUP } ; SWAP ; DROP } ;
-                      SWAP ;
-                      DIP { DIP { DROP } } ;
-                      DUP ;
-                      CDR ;
-                      DIP { DIP 2 { DUP } ; DIG 2 ; DROP } ;
-                      DIP 3 { DROP } ;
-                      DUG 2 ;
-                      DROP ;
-                      DIP { DUP } ;
-                      SWAP ;
-                      DIP { DIP 4 { DUP } ; DIG 4 ; CDR ; CDR } ;
-                      COMPARE ;
-                      LT ;
-                      IF { PUSH string "Not enough signatures passed the check" ; FAILWITH }
-                         { DIP 4 { DUP } ;
-                           DIG 4 ;
-                           CAR ;
-                           CDR ;
-                           PUSH nat 1 ;
-                           ADD ;
-                           DIP { DIP 4 { DUP } ; DIG 4 ; DUP ; CDR ; SWAP ; CAR ; CAR } ;
-                           SWAP ;
-                           PAIR ;
-                           PAIR ;
-                           DIP 5 { DROP } ;
-                           DUG 4 ;
-                           PUSH unit Unit } ;
-                      DIP { DROP 3 } } ;
-                 DROP ;
-                 DUP ;
-                 UNIT ;
-                 EXEC ;
-                 DIP { DIP { DUP } ; SWAP } ;
-                 PAIR ;
-                 DIP { DROP 4 } } ;
-             SWAP ;
              CAR ;
-             DIP 2 { DUP } ;
-             DIG 2 ;
+             DIP { DUP ; CDR } ;
+             PAIR ;
+             DUP ;
+             CAR ;
+             DIP { DUP } ;
+             SWAP ;
              CDR ;
              DIP { DUP } ;
              SWAP ;
+             CAR ;
+             CDR ;
+             DIP 2 { DUP } ;
+             DIG 2 ;
+             CAR ;
+             CAR ;
+             DIP { DIP { DUP } ; SWAP ; CAR ; CDR } ;
+             COMPARE ;
+             NEQ ;
+             IF { PUSH string "Counters does not match" ; FAILWITH }
+                { DUP ;
+                  DIP { DIP 2 { DUP } ; DIG 2 ; CAR ; CAR } ;
+                  PAIR ;
+                  DIP { DIP { DUP } ; SWAP ; CDR ; CAR ; CHAIN_ID ; SWAP ; PAIR } ;
+                  PAIR ;
+                  PACK ;
+                  PUSH nat 0 ;
+                  DIP 3 { DUP } ;
+                  DIG 3 ;
+                  CAR ;
+                  CAR ;
+                  DIP 5 { DUP } ;
+                  DIG 5 ;
+                  CDR ;
+                  DIP { DUP ; DIP { DIP { DUP } ; SWAP } ; PAIR } ;
+                  ITER { SWAP ;
+                         PAIR ;
+                         DUP ;
+                         CAR ;
+                         DIP { DUP } ;
+                         SWAP ;
+                         CDR ;
+                         DIP { DUP } ;
+                         SWAP ;
+                         CAR ;
+                         IF_CONS
+                           { DIP { DUP } ;
+                             SWAP ;
+                             DIP { DIP 3 { DUP } ; DIG 3 ; CDR } ;
+                             PAIR ;
+                             DIP 4 { DROP } ;
+                             DUG 3 ;
+                             DIP 2 { DUP } ;
+                             DIG 2 ;
+                             CAR ;
+                             DIP { DUP ; HASH_KEY } ;
+                             COMPARE ;
+                             EQ ;
+                             IF { DUP ;
+                                  DIP { DIP 2 { DUP } ; DIG 2 ; CDR ; DIP { DIP 7 { DUP } ; DIG 7 } } ;
+                                  CHECK_SIGNATURE ;
+                                  IF { DIP 3 { DUP } ;
+                                       DIG 3 ;
+                                       CDR ;
+                                       PUSH nat 1 ;
+                                       ADD ;
+                                       DIP { DIP 3 { DUP } ; DIG 3 ; CAR } ;
+                                       SWAP ;
+                                       PAIR ;
+                                       DIP 4 { DROP } ;
+                                       DUG 3 ;
+                                       PUSH unit Unit }
+                                     { PUSH string "Invalid signature" ; FAILWITH } }
+                                { PUSH unit Unit } ;
+                             DIP { DROP 2 } }
+                           { PUSH unit Unit } ;
+                         DROP ;
+                         DIP { DUP } ;
+                         SWAP ;
+                         DIP { DROP 3 } } ;
+                  DUP ;
+                  CAR ;
+                  DIP { DIP { DUP } ; SWAP ; DROP } ;
+                  SWAP ;
+                  DIP { DIP { DROP } } ;
+                  DUP ;
+                  CDR ;
+                  DIP { DIP 2 { DUP } ; DIG 2 ; DROP } ;
+                  DIP 3 { DROP } ;
+                  DUG 2 ;
+                  DROP ;
+                  DIP { DUP } ;
+                  SWAP ;
+                  DIP { DIP 4 { DUP } ; DIG 4 ; CDR ; CDR } ;
+                  COMPARE ;
+                  LT ;
+                  IF { PUSH string "Not enough signatures passed the check" ; FAILWITH }
+                     { DIP 4 { DUP } ;
+                       DIG 4 ;
+                       CAR ;
+                       CDR ;
+                       PUSH nat 1 ;
+                       ADD ;
+                       DIP { DIP 4 { DUP } ; DIG 4 ; DUP ; CDR ; SWAP ; CAR ; CAR } ;
+                       SWAP ;
+                       PAIR ;
+                       PAIR ;
+                       DIP 5 { DROP } ;
+                       DUG 4 ;
+                       PUSH unit Unit } ;
+                  DIP { DROP 3 } } ;
+             DROP ;
              DUP ;
+             UNIT ;
+             EXEC ;
              DIP { DIP { DUP } ; SWAP } ;
              PAIR ;
-             DIP { DIP 3 { DUP } ; DIG 3 } ;
-             EXEC ;
              DIP { DROP 5 } } } |} ]
 
 let%expect_test _ =
@@ -457,91 +399,72 @@ let%expect_test _ =
         (pair (pair (set %auth address) (big_map %message_store bytes (set address)))
               (nat %threshold)) ;
       code { DUP ;
-             LAMBDA
-               (pair (lambda unit (list operation))
-                     (pair (pair (set %auth address) (big_map %message_store bytes (set address)))
-                           (nat %threshold)))
-               (pair (list operation)
-                     (pair (pair (set %auth address) (big_map %message_store bytes (set address)))
-                           (nat %threshold)))
-               { DUP ;
-                 CAR ;
-                 DIP { DUP } ;
-                 SWAP ;
-                 CDR ;
-                 DUP ;
-                 CAR ;
-                 CAR ;
-                 SENDER ;
-                 MEM ;
-                 NOT ;
-                 IF { PUSH string "Unauthorized address" ; FAILWITH } { PUSH unit Unit } ;
-                 DROP ;
-                 DIP { DUP } ;
-                 SWAP ;
-                 DUP ;
-                 PACK ;
-                 DUP ;
-                 NIL operation ;
-                 SWAP ;
-                 DIP { DIP 3 { DUP } ; DIG 3 ; CAR ; CDR } ;
-                 GET ;
-                 IF_NONE
-                   { EMPTY_SET address }
-                   { DUP ; PUSH bool True ; SENDER ; UPDATE ; DIP { DROP } } ;
-                 DUP ;
-                 SIZE ;
-                 DIP { DIP 4 { DUP } ; DIG 4 ; CDR } ;
-                 COMPARE ;
-                 GE ;
-                 IF { DIP 2 { DUP } ;
-                      DIG 2 ;
-                      DIP { DIP 4 { DUP } ; DIG 4 ; CAR ; CDR ; NONE (set address) } ;
-                      UPDATE ;
-                      DIP { DIP 4 { DUP } ; DIG 4 ; DUP ; CDR ; SWAP ; CAR ; CAR } ;
-                      SWAP ;
-                      PAIR ;
-                      PAIR ;
-                      DIP 5 { DROP } ;
-                      DUG 4 ;
-                      DIP 3 { DUP } ;
-                      DIG 3 ;
-                      UNIT ;
-                      EXEC ;
-                      DIP { DIP { DUP } ; SWAP ; DROP } ;
-                      SWAP ;
-                      DIP { DIP { DROP } } ;
-                      PUSH unit Unit }
-                    { DIP 2 { DUP } ;
-                      DIG 2 ;
-                      DIP { DUP ; SOME ; DIP { DIP 4 { DUP } ; DIG 4 ; CAR ; CDR } } ;
-                      UPDATE ;
-                      DIP { DIP 4 { DUP } ; DIG 4 ; DUP ; CDR ; SWAP ; CAR ; CAR } ;
-                      SWAP ;
-                      PAIR ;
-                      PAIR ;
-                      DIP 5 { DROP } ;
-                      DUG 4 ;
-                      PUSH unit Unit } ;
-                 DROP ;
-                 DIP { DUP } ;
-                 SWAP ;
-                 DIP { DIP 4 { DUP } ; DIG 4 } ;
-                 PAIR ;
-                 DIP { DROP 7 } } ;
-             SWAP ;
              CAR ;
-             DIP 2 { DUP } ;
-             DIG 2 ;
+             DIP { DUP ; CDR } ;
+             PAIR ;
+             DUP ;
              CDR ;
+             DUP ;
+             CAR ;
+             CAR ;
+             SENDER ;
+             MEM ;
+             NOT ;
+             IF { PUSH string "Unauthorized address" ; FAILWITH } { PUSH unit Unit } ;
+             DROP ;
              DIP { DUP } ;
              SWAP ;
+             CAR ;
              DUP ;
-             DIP { DIP { DUP } ; SWAP } ;
+             PACK ;
+             DUP ;
+             NIL operation ;
+             SWAP ;
+             DIP { DIP 3 { DUP } ; DIG 3 ; CAR ; CDR } ;
+             GET ;
+             IF_NONE
+               { EMPTY_SET address }
+               { DUP ; PUSH bool True ; SENDER ; UPDATE ; DIP { DROP } } ;
+             DUP ;
+             SIZE ;
+             DIP { DIP 4 { DUP } ; DIG 4 ; CDR } ;
+             COMPARE ;
+             GE ;
+             IF { DIP 2 { DUP } ;
+                  DIG 2 ;
+                  DIP { DIP 4 { DUP } ; DIG 4 ; CAR ; CDR ; NONE (set address) } ;
+                  UPDATE ;
+                  DIP { DIP 4 { DUP } ; DIG 4 ; DUP ; CDR ; SWAP ; CAR ; CAR } ;
+                  SWAP ;
+                  PAIR ;
+                  PAIR ;
+                  DIP 5 { DROP } ;
+                  DUG 4 ;
+                  DIP 3 { DUP } ;
+                  DIG 3 ;
+                  UNIT ;
+                  EXEC ;
+                  DIP { DIP { DUP } ; SWAP ; DROP } ;
+                  SWAP ;
+                  DIP { DIP { DROP } } ;
+                  PUSH unit Unit }
+                { DIP 2 { DUP } ;
+                  DIG 2 ;
+                  DIP { DUP ; SOME ; DIP { DIP 4 { DUP } ; DIG 4 ; CAR ; CDR } } ;
+                  UPDATE ;
+                  DIP { DIP 4 { DUP } ; DIG 4 ; DUP ; CDR ; SWAP ; CAR ; CAR } ;
+                  SWAP ;
+                  PAIR ;
+                  PAIR ;
+                  DIP 5 { DROP } ;
+                  DUG 4 ;
+                  PUSH unit Unit } ;
+             DROP ;
+             DIP { DUP } ;
+             SWAP ;
+             DIP { DIP 4 { DUP } ; DIG 4 } ;
              PAIR ;
-             DIP { DIP 3 { DUP } ; DIG 3 } ;
-             EXEC ;
-             DIP { DROP 5 } } } |} ]
+             DIP { DROP 7 } } } |} ]
 
 let%expect_test _ =
   run_ligo_good [ "compile-contract" ; contract "vote.mligo" ; "main" ] ;
@@ -555,17 +478,10 @@ let%expect_test _ =
         (pair (pair (pair (timestamp %beginning_time) (map %candidates string int))
                     (pair (timestamp %finish_time) (string %title)))
               (set %voters address)) ;
-      code { LAMBDA
-               (pair (pair (pair (timestamp %beginning_time) (timestamp %finish_time)) (string %title))
-                     (pair (pair (pair (timestamp %beginning_time) (map %candidates string int))
-                                 (pair (timestamp %finish_time) (string %title)))
-                           (set %voters address)))
-               (pair (list operation)
-                     (pair (pair (pair (timestamp %beginning_time) (map %candidates string int))
-                                 (pair (timestamp %finish_time) (string %title)))
-                           (set %voters address)))
+      code { DUP ;
+             CAR ;
+             IF_LEFT
                { DUP ;
-                 CAR ;
                  PUSH int 0 ;
                  SOME ;
                  DIP { PUSH int 0 ;
@@ -594,17 +510,11 @@ let%expect_test _ =
                  PAIR ;
                  NIL operation ;
                  PAIR ;
-                 DIP { DROP 3 } } ;
-             LAMBDA
-               (pair string
-                     (pair (pair (pair (timestamp %beginning_time) (map %candidates string int))
-                                 (pair (timestamp %finish_time) (string %title)))
-                           (set %voters address)))
-               (pair (list operation)
-                     (pair (pair (pair (timestamp %beginning_time) (map %candidates string int))
-                                 (pair (timestamp %finish_time) (string %title)))
-                           (set %voters address)))
+                 DIP { DROP 3 } }
                { DUP ;
+                 DIP { DIP { DUP } ; SWAP ; CDR } ;
+                 PAIR ;
+                 DUP ;
                  CAR ;
                  DIP { DUP } ;
                  SWAP ;
@@ -645,28 +555,5 @@ let%expect_test _ =
                  PAIR ;
                  NIL operation ;
                  PAIR ;
-                 DIP { DROP 6 } } ;
-             DIP 2 { DUP } ;
-             DIG 2 ;
-             CAR ;
-             DIP 3 { DUP } ;
-             DIG 3 ;
-             CDR ;
-             DIP { DUP } ;
-             SWAP ;
-             IF_LEFT
-               { DUP ;
-                 DUP ;
-                 DIP { DIP 2 { DUP } ; DIG 2 } ;
-                 PAIR ;
-                 DIP { DIP 5 { DUP } ; DIG 5 } ;
-                 EXEC ;
-                 DIP { DROP 2 } }
-               { DUP ;
-                 DUP ;
-                 DIP { DIP 2 { DUP } ; DIG 2 } ;
-                 PAIR ;
-                 DIP { DIP 4 { DUP } ; DIG 4 } ;
-                 EXEC ;
-                 DIP { DROP 2 } } ;
-             DIP { DROP 5 } } } |}]
+                 DIP { DROP 7 } } ;
+             DIP { DROP } } } |}]
diff --git a/src/main/compile/of_mini_c.ml b/src/main/compile/of_mini_c.ml
index d8419b435..e6dbc3cf3 100644
--- a/src/main/compile/of_mini_c.ml
+++ b/src/main/compile/of_mini_c.ml
@@ -22,17 +22,17 @@ let compile_function = fun e ->
 
 let compile_expression_as_function_entry = fun program name ->
   let%bind aggregated = aggregate_entry program name true in
-  let%bind aggregated = Self_mini_c.all_expression aggregated in
+  let aggregated = Self_mini_c.all_expression aggregated in
   compile_function aggregated
 
 let compile_function_entry = fun program name ->
   let%bind aggregated = aggregate_entry program name false in
-  let%bind aggregated = Self_mini_c.all_expression aggregated in
+  let aggregated = Self_mini_c.all_expression aggregated in
   compile_function aggregated
 
 let compile_contract_entry = fun program name ->
   let%bind aggregated = aggregate_entry program name false in
-  let%bind aggregated = Self_mini_c.all_expression aggregated in
+  let aggregated = Self_mini_c.all_expression aggregated in
   let%bind compiled = compile_function aggregated in
   let%bind (param_ty , storage_ty) =
     let%bind fun_ty = get_t_function aggregated.type_value in
diff --git a/src/passes/4-typer-new/solver.ml b/src/passes/4-typer-new/solver.ml
index af7a68c38..554f1af07 100644
--- a/src/passes/4-typer-new/solver.ml
+++ b/src/passes/4-typer-new/solver.ml
@@ -706,13 +706,6 @@ let propagator_break_ctor : output_break_ctor propagator =
 type output_specialize1 = { poly : c_poly_simpl ; a_k_var : c_constructor_simpl }
 
 
-module Int = struct
-  (* Restrict use of Pervasives.compare to just `int`, because we
-     don't want to risk the type of a field changing from int to
-     something not compatible with Pervasives.compare, and not
-     noticing that the comparator needs to be updated. *)
-  let compare (a : int) (b : int) = Pervasives.compare a b
-end
 let (<?) ca cb =
   if ca = 0 then cb () else ca
 let rec compare_list f = function
diff --git a/src/passes/6-transpiler/transpiler.ml b/src/passes/6-transpiler/transpiler.ml
index 521d531fa..4e7554863 100644
--- a/src/passes/6-transpiler/transpiler.ml
+++ b/src/passes/6-transpiler/transpiler.ml
@@ -2,6 +2,8 @@
 
 For more info, see back-end.md: https://gitlab.com/ligolang/ligo/blob/dev/gitlab-pages/docs/contributors/big-picture/back-end.md *)
 
+(* TODO(tomjack) all Var.of_name are suspicious, continue war against string? *)
+
 open! Trace
 open Helpers
 
@@ -267,14 +269,14 @@ and transpile_annotated_expression (ae:AST.annotated_expression) : expression re
   | E_let_in {binder; rhs; result} ->
     let%bind rhs' = transpile_annotated_expression rhs in
     let%bind result' = transpile_annotated_expression result in
-    return (E_let_in ((binder, rhs'.type_value), rhs', result'))
+    return (E_let_in ((Var.of_name binder, rhs'.type_value), rhs', result'))
   | E_literal l -> return @@ E_literal (transpile_literal l)
   | E_variable name -> (
       let%bind ele =
         trace_option (corner_case ~loc:__LOC__ "name not in environment") @@
         AST.Environment.get_opt name ae.environment in
       let%bind tv = transpile_environment_element_type ele in
-      return ~tv @@ E_variable name
+      return ~tv @@ E_variable (Var.of_name name)
     )
   | E_application (a, b) ->
       let%bind a = transpile_annotated_expression a in
@@ -377,7 +379,7 @@ and transpile_annotated_expression (ae:AST.annotated_expression) : expression re
           let%bind body' = transpile_annotated_expression l.body in
           let%bind (input , _) = AST.get_t_function f.type_annotation in
           let%bind input' = transpile_type input in
-          ok ((l.binder , input') , body')
+          ok ((Var.of_name l.binder , input') , body')
         in
         let expression_to_iterator_body (f : AST.annotated_expression) =
           match f.expression with
@@ -520,7 +522,7 @@ and transpile_annotated_expression (ae:AST.annotated_expression) : expression re
       in
       let%bind (_, path) = bind_fold_right_list aux (ty, []) path in
       let%bind expr' = transpile_annotated_expression expr in
-      return (E_assignment (typed_name.type_name, path, expr'))
+      return (E_assignment (Var.of_name typed_name.type_name, path, expr'))
     )
   | E_matching (expr, m) -> (
       let%bind expr' = transpile_annotated_expression expr in
@@ -535,7 +537,7 @@ and transpile_annotated_expression (ae:AST.annotated_expression) : expression re
             let%bind s' = transpile_annotated_expression s in
             ok (tv' , s')
           in
-          return @@ E_if_none (expr' , n , ((name , tv') , s'))
+          return @@ E_if_none (expr' , n , ((Var.of_name name , tv') , s'))
       | Match_list {
           match_nil ;
           match_cons = (((hd_name , hd_ty) , (tl_name , tl_ty)) , match_cons) ;
@@ -545,7 +547,7 @@ and transpile_annotated_expression (ae:AST.annotated_expression) : expression re
             let%bind hd_ty' = transpile_type hd_ty in
             let%bind tl_ty' = transpile_type tl_ty in
             let%bind match_cons' = transpile_annotated_expression match_cons in
-            ok (((hd_name , hd_ty') , (tl_name , tl_ty')) , match_cons')
+            ok (((Var.of_name hd_name , hd_ty') , (Var.of_name tl_name , tl_ty')) , match_cons')
           in
           return @@ E_if_cons (expr' , nil , cons)
         )
@@ -577,19 +579,19 @@ and transpile_annotated_expression (ae:AST.annotated_expression) : expression re
                   trace_option (corner_case ~loc:__LOC__ "missing match clause") @@
                   List.find_opt (fun ((constructor_name' , _) , _) -> constructor_name' = constructor_name) lst in
                 let%bind body' = transpile_annotated_expression body in
-                return @@ E_let_in ((name , tv) , top , body')
+                return @@ E_let_in ((Var.of_name name , tv) , top , body')
               )
             | ((`Node (a , b)) , tv) ->
                 let%bind a' =
                   let%bind a_ty = get_t_left tv in
-                  let a_var = "left" , a_ty in
-                  let%bind e = aux (((Expression.make (E_variable "left") a_ty))) a in
+                  let a_var = Var.of_name "left" , a_ty in
+                  let%bind e = aux (((Expression.make (E_variable (Var.of_name "left")) a_ty))) a in
                   ok (a_var , e)
                 in
                 let%bind b' =
                   let%bind b_ty = get_t_right tv in
-                  let b_var = "right" , b_ty in
-                  let%bind e = aux (((Expression.make (E_variable "right") b_ty))) b in
+                  let b_var = Var.of_name "right" , b_ty in
+                  let%bind e = aux (((Expression.make (E_variable (Var.of_name "right")) b_ty))) b in
                   ok (b_var , e)
                 in
                 return @@ E_if_left (top , a' , b')
@@ -606,7 +608,7 @@ and transpile_lambda l (input_type , output_type) =
   let%bind input = transpile_type input_type in
   let%bind output = transpile_type output_type in
   let tv = Combinators.t_function input output in
-  let closure = E_closure { binder ; body = result'} in
+  let closure = E_closure { binder = Var.of_name binder ; body = result'} in
   ok @@ Combinators.Expression.make_tpl (closure , tv)
 
 let transpile_declaration env (d:AST.declaration) : toplevel_statement result =
@@ -614,8 +616,8 @@ let transpile_declaration env (d:AST.declaration) : toplevel_statement result =
   | Declaration_constant ({name;annotated_expression} , _) ->
       let%bind expression = transpile_annotated_expression annotated_expression in
       let tv = Combinators.Expression.get_type expression in
-      let env' = Environment.add (name, tv) env in
-      ok @@ ((name, expression), environment_wrap env env')
+      let env' = Environment.add (Var.of_name name, tv) env in
+      ok @@ ((Var.of_name name, expression), environment_wrap env env')
 
 let transpile_program (lst : AST.program) : program result =
   let aux (prev:(toplevel_statement list * Environment.t) result) cur =
diff --git a/src/passes/7-self_mini_c/dune b/src/passes/7-self_mini_c/dune
index ec9f97639..da1927e25 100644
--- a/src/passes/7-self_mini_c/dune
+++ b/src/passes/7-self_mini_c/dune
@@ -4,8 +4,9 @@
   (libraries
     mini_c
   )
+  (inline_tests)
   (preprocess
-    (pps ppx_let)
+    (pps ppx_let ppx_expect)
   )
   (flags (:standard -w +1..62-4-9-44-40-42-48-30@39@33 -open Simple_utils ))
 )
diff --git a/src/passes/7-self_mini_c/self_mini_c.ml b/src/passes/7-self_mini_c/self_mini_c.ml
index af24dae97..4dbd2573b 100644
--- a/src/passes/7-self_mini_c/self_mini_c.ml
+++ b/src/passes/7-self_mini_c/self_mini_c.ml
@@ -1,8 +1,17 @@
 open Mini_c
-open Trace
+open! Trace
 
-(* Overly conservative purity test: ok to treat pure things as impure,
-   must not treat impure things as pure. *)
+(* TODO hack to specialize map_expression to identity monad *)
+let map_expression :
+  (expression -> expression) -> (expression -> expression) =
+  fun f e ->
+  match Helpers.map_expression (fun e -> ok (f e)) e with
+  | Ok (e, _) -> e
+  | Error _ -> assert false (* impossible *)
+
+
+(* Conservative purity test: ok to treat pure things as impure, must
+   not treat impure things as pure. *)
 
 (* true if the name names a pure constant -- i.e. if uses will be pure
    assuming arguments are pure *)
@@ -54,25 +63,177 @@ let rec is_pure : expression -> bool = fun e ->
   (* definitely not pure *)
   | E_assignment _ -> false
 
+let occurs_in : Var.t -> expression -> bool =
+  fun x e ->
+  let fvs = Free_variables.expression [] e in
+  Free_variables.mem x fvs
 
-(* Eliminate dead `let` with pure rhs *)
+let occurs_count : Var.t -> expression -> int =
+  fun x e ->
+  let fvs = Free_variables.expression [] e in
+  Free_variables.mem_count x fvs
 
-let rec elim_dead_code : expression -> expression result = fun e ->
-  let changed = ref false in (* ugh *)
-  let mapper : Helpers.mapper = fun e ->
-    match e.content with
-    | E_let_in ((x, _), e1, e2) when is_pure e1 ->
-      let fvs = Free_variables.expression [] e2 in
-      if Free_variables.mem x fvs
-      then ok e
-      else
-        (* pure e1 is not used, eliminate! *)
-        (changed := true ; ok e2)
-    | _ -> ok e in
-  let%bind e = Helpers.map_expression mapper e in
+(* If `ignore_lambdas` is true, ignore assignments which occur inside
+   lambdas, which have no effect on the value of the variable outside
+   of the lambda. *)
+let rec is_assigned : ignore_lambdas:bool -> Var.t -> expression -> bool =
+  fun ~ignore_lambdas x e ->
+  let self = is_assigned ~ignore_lambdas x in
+  let selfs = List.exists self in
+  let it = Var.equal x in
+  let self_binder binder body =
+    if it binder
+    then false
+    else self body in
+  let self_binder2 binder1 binder2 body =
+    if it binder1 || it binder2
+    then false
+    else self body in
+  match e.content with
+  | E_assignment (x, _, e) ->
+    it x || self e
+  | E_closure { binder; body } ->
+    if ignore_lambdas
+    then false
+    else self_binder binder body
+  | E_constant (_, args) ->
+    selfs args
+  | E_application (f, arg) ->
+    selfs [ f ; arg ]
+  | E_iterator (_, ((x, _), e1), e2) ->
+    self_binder x e1 || self e2
+  | E_fold (((x, _), e1), e2, e3) ->
+    self_binder x e1 || selfs [ e2 ; e3 ]
+  | E_if_bool (e1, e2, e3) ->
+    selfs [ e1 ; e2 ; e3 ]
+  | E_if_none (e1, e2, ((x, _), e3)) ->
+    selfs [ e1 ; e2 ] || self_binder x e3
+  | E_if_cons (e1, e2, (((hd, _), (tl, _)), e3)) ->
+    selfs [ e1 ; e2 ] || self_binder2 hd tl e3
+  | E_if_left (e1, ((l, _), e2), ((r, _), e3)) ->
+    self e1 || self_binder l e2 || self_binder r e3
+  | E_let_in ((x, _), e1, e2) ->
+    self e1 || self_binder x e2
+  | E_sequence (e1, e2) ->
+    selfs [ e1 ; e2 ]
+  | E_while (e1, e2) ->
+    selfs [ e1 ; e2 ]
+  | E_literal _
+  | E_skip
+  | E_variable _
+  | E_make_empty_map _
+  | E_make_empty_big_map _
+  | E_make_empty_list _
+  | E_make_empty_set _
+  | E_make_none _ ->
+    false
+
+(* Let "inlining" mean transforming the code:
+
+     let x = e1 in e2
+
+   to:
+
+     e2[e1/x]
+
+   (where the latter signifies substituting e1 for x in e2.)
+
+   Things which can go wrong for inlining:
+
+   - If `e1` is not pure, inlining may fail to preserve semantics.
+   - If assignments to `x` occur in e2, inlining does not make sense.
+   - Free variables of `e1` may be assigned in e2, before usages of `x`.
+   - Free variables of `e1` may be shadowed in e2, at usages of `x`. This
+     is not a problem if the substitution is capture-avoiding.
+   - ?
+*)
+
+let can_inline : Var.t -> expression -> expression -> bool =
+  fun x e1 e2 ->
+  is_pure e1 &&
+  (* if x does not occur in e2, there can be no other problems:
+     substitution will be a noop up to alpha-equivalence *)
+  (not (occurs_in x e2) ||
+   (* else, must worry about assignment *)
+   (not (is_assigned ~ignore_lambdas:false x e2) &&
+    List.for_all
+      (fun y -> not (is_assigned ~ignore_lambdas:true y e2))
+      (Free_variables.expression [] e2)))
+
+let should_inline : Var.t -> expression -> bool =
+  fun x e ->
+  occurs_count x e <= 1
+
+let inline_let : bool ref -> expression -> expression =
+  fun changed e ->
+  match e.content with
+  | E_let_in ((x, _a), e1, e2) ->
+    if can_inline x e1 e2 && should_inline x e2
+    then
+      (* can raise Subst.Bad_argument, but should not happen, due to
+         can_inline *)
+      let e2' = Subst.subst_expression ~body:e2 ~x:x ~expr:e1 in
+      (changed := true ; e2')
+    else
+      e
+  | _ -> e
+
+let inline_lets : bool ref -> expression -> expression =
+  fun changed ->
+  map_expression (inline_let changed)
+
+
+(* Let "beta" mean transforming the code:
+
+     (\x. e1) e2
+
+   to:
+
+     let x = e2 in e1
+
+   Things which can go wrong for beta reduction:
+
+   - If e1 contains (meaningful) assignments to free variables, semantics
+     will not be preserved.
+   - ?
+*)
+
+let can_beta : anon_function -> bool =
+  fun lam ->
+  List.for_all
+    (fun x -> not (is_assigned ~ignore_lambdas:true x lam.body))
+    (Free_variables.lambda [] lam)
+
+let beta : bool ref -> expression -> expression =
+  fun changed e ->
+  match e.content with
+  | E_application ({ content = E_closure { binder = x ; body = e1 } ; type_value = T_function (xtv, tv) }, e2) ->
+    if can_beta { binder = x ; body = e1 }
+    then
+      (changed := true ;
+       Expression.make (E_let_in ((x, xtv), e2, e1)) tv)
+    else e
+
+  (* also do CAR (PAIR x y) ↦ x, or CDR (PAIR x y) ↦ y, only if x and y are pure *)
+  | E_constant ("CAR"|"CDR" as const, [ { content = E_constant ("PAIR", [ e1 ; e2 ]) ; type_value = _ } ]) ->
+    if is_pure e1 && is_pure e2
+    then (changed := true ;
+          match const with
+          | "CAR" -> e1
+          | "CDR" -> e2
+          | _ -> assert false)
+    else e
+  | _ -> e
+
+let betas : bool ref -> expression -> expression =
+  fun changed ->
+  map_expression (beta changed)
+
+let rec all_expression : expression -> expression =
+  fun e ->
+  let changed = ref false in
+  let e = inline_lets changed e in
+  let e = betas changed e in
   if !changed
-  then elim_dead_code e
-  else ok e
-
-let all_expression : expression -> expression result =
-  elim_dead_code
+  then all_expression e
+  else e
diff --git a/src/passes/7-self_mini_c/subst.ml b/src/passes/7-self_mini_c/subst.ml
new file mode 100644
index 000000000..7f6eb0209
--- /dev/null
+++ b/src/passes/7-self_mini_c/subst.ml
@@ -0,0 +1,430 @@
+open Mini_c
+
+(* Reference implementation:
+   https://www.cs.cornell.edu/courses/cs3110/2019sp/textbook/interp/lambda-subst/main.ml
+
+   ...but, it has at least one bug: in subst,
+   `let new_body = replace e' y fresh in ...` should be:
+   `let new_body = replace e' fresh y in ...`,
+   due to the arg order choice for replace.
+
+   Below, this bug is fixed by adopting the other order choice for
+   replace (as well as subst).  *)
+
+
+(* replace in `e` the variable `x` with `y`.
+
+   It would be fine -- better? -- to only replace the _free_ x.
+*)
+let rec replace : expression -> var_name -> var_name -> expression =
+  fun e x y ->
+  let replace e = replace e x y in
+  let return content = { e with content } in
+  let replace_var v =
+    if Var.equal v x
+    then y
+    else v in
+  match e.content with
+  | E_literal _ -> e
+  | E_closure { binder ; body } ->
+    let body = replace body in
+    let binder = replace_var binder in
+    return @@ E_closure { binder ; body }
+  | E_skip -> e
+  | E_constant (c, args) ->
+    let args = List.map replace args in
+    return @@ E_constant (c, args)
+  | E_application (f, x) ->
+    let (f, x) = Tuple.map2 replace (f, x) in
+    return @@ E_application (f, x)
+  | E_variable z ->
+    let z = replace_var z in
+    return @@ E_variable z
+  | E_make_empty_map _ -> e
+  | E_make_empty_big_map _ -> e
+  | E_make_empty_list _ -> e
+  | E_make_empty_set _ -> e
+  | E_make_none _ -> e
+  | E_iterator (name, ((v, tv), body), expr) ->
+    let body = replace body in
+    let expr = replace expr in
+    let v = replace_var v in
+    return @@ E_iterator (name, ((v, tv), body), expr)
+  | E_fold (((v, tv), body), collection, initial) ->
+    let body = replace body in
+    let collection = replace collection in
+    let initial = replace initial in
+    let v = replace_var v in
+    return @@ E_fold (((v, tv), body), collection, initial)
+  | E_if_bool (c, bt, bf) ->
+    let c = replace c in
+    let bt = replace bt in
+    let bf = replace bf in
+    return @@ E_if_bool (c, bt, bf)
+  | E_if_none (c, bt, ((v, tv), bf)) ->
+    let c = replace c in
+    let bt = replace bt in
+    let bf = replace bf in
+    let v = replace_var v in
+    return @@ E_if_none (c, bt, ((v, tv), bf))
+  | E_if_cons (c, bf, (((v1, tv1), (v2, tv2)), bt)) ->
+    let c = replace c in
+    let bf = replace bf in
+    let v1 = replace_var v1 in
+    let v2 = replace_var v2 in
+    let bt = replace bt in
+    return @@ E_if_cons (c, bf, (((v1, tv1), (v2, tv2)), bt))
+  | E_if_left (c, ((v1, tv1), bt), ((v2, tv2), bf)) ->
+    let c = replace c in
+    let bf = replace bf in
+    let v1 = replace_var v1 in
+    let v2 = replace_var v2 in
+    let bt = replace bt in
+    return @@ E_if_left (c, ((v1, tv1), bt), ((v2, tv2), bf))
+  | E_let_in ((v, tv), e1, e2) ->
+    let v = replace_var v in
+    let e1 = replace e1 in
+    let e2 = replace e2 in
+    return @@ E_let_in ((v, tv), e1, e2)
+  | E_sequence (e1, e2) ->
+    let e1 = replace e1 in
+    let e2 = replace e2 in
+    return @@ E_sequence (e1, e2)
+  | E_assignment (v, path, e) ->
+    let v = replace_var v in
+    let e = replace e in
+    return @@ E_assignment (v, path, e)
+  | E_while (cond, body) ->
+    let cond = replace cond in
+    let body = replace body in
+    return @@ E_while (cond, body)
+
+(**
+   Computes `body[x := expr]`.
+   This raises Bad_argument in the case of assignments with a name clash. (`x <- 42[x := 23]` makes no sense.)
+**)
+exception Bad_argument
+let rec subst_expression : body:expression -> x:var_name -> expr:expression -> expression =
+  fun ~body ~x ~expr ->
+  let self body = subst_expression ~body ~x ~expr in
+  let subst_binder y expr' =
+    (* if x is shadowed, binder doesn't change *)
+    if Var.equal x y
+    then (y, expr')
+    (* else, if no capture, subst in binder *)
+    else if not (Free_variables.mem y (Free_variables.expression [] expr))
+    then (y, self expr')
+    (* else, avoid capture and subst in binder *)
+    else
+      let fresh = Var.fresh_like y in
+      let new_body = replace expr' y fresh in
+      (fresh, self new_body) in
+  (* hack to avoid reimplementing subst_binder for 2-ary binder in E_if_cons:
+     intuitively, we substitute in \hd tl. expr' as if it were \hd. \tl. expr *)
+  let subst_binder2 y z expr' =
+    let dummy = T_base Base_unit in
+    let hack = { content = E_closure { binder = z ; body = expr' } ;
+                 type_value = dummy } in
+    match subst_binder y hack with
+    | (y', { content = E_closure { binder = z' ; body = body } ; type_value = _dummy }) ->
+      (y', z', { body with type_value = expr'.type_value })
+    | _ -> assert false in
+  let return content = {body with content} in
+  let return_id = body in
+  match body.content with
+  | E_variable x' ->
+     if x' = x
+     then expr
+     else return_id
+  | E_closure { binder; body } -> (
+    let (binder, body) = subst_binder binder body in
+    return @@ E_closure { binder ; body }
+  )
+  | E_let_in ((v , tv) , expr , body) -> (
+    let expr = self expr in
+    let (v, body) = subst_binder v body in
+    return @@ E_let_in ((v , tv) , expr , body)
+  )
+  | E_iterator (s, ((name , tv) , body) , collection) -> (
+    let (name, body) = subst_binder name body in
+    let collection = self collection in
+    return @@ E_iterator (s, ((name , tv) , body) , collection)
+  )
+  | E_fold (((name , tv) , body) , collection , init) -> (
+    let (name, body) = subst_binder name body in
+    let collection = self collection in
+    let init = self init in
+    return @@ E_fold (((name , tv) , body) , collection , init)
+  )
+  | E_if_none (c, n, ((name, tv) , s)) -> (
+    let c = self c in
+    let n = self n in
+    let (name, s) = subst_binder name s in
+    return @@ E_if_none (c, n, ((name, tv) , s))
+  )
+  | E_if_cons (c, n, (((hd, hdtv) , (tl, tltv)) , cons)) -> (
+    let c = self c in
+    let n = self n in
+    let (hd, tl, cons) = subst_binder2 hd tl cons in
+    return @@ E_if_cons (c, n, (((hd, hdtv) , (tl, tltv)) , cons))
+  )
+  | E_if_left (c, ((name_l, tvl) , l), ((name_r, tvr) , r)) -> (
+    let c = self c in
+    let (name_l, l) = subst_binder name_l l in
+    let (name_r, r) = subst_binder name_r r in
+    return @@ E_if_left (c, ((name_l, tvl) , l), ((name_r, tvr) , r))
+  )
+  (* All that follows is boilerplate *)
+  | E_literal _ | E_skip | E_make_none _
+  | E_make_empty_map (_,_)
+  | E_make_empty_big_map _
+  | E_make_empty_list _
+  | E_make_empty_set _ as em -> return em
+  | E_constant (name, lst) -> (
+      let lst' = List.map self lst in
+      return @@ E_constant (name,lst')
+  )
+  | E_application farg -> (
+      let farg' = Tuple.map2 self farg in
+      return @@ E_application farg'
+  )
+  | E_while eb -> (
+      let eb' = Tuple.map2 self eb in
+      return @@ E_while eb'
+  )
+  | E_if_bool cab -> (
+      let cab' = Tuple.map3 self cab in
+      return @@ E_if_bool cab'
+  )
+  | E_sequence ab -> (
+      let ab' = Tuple.map2 self ab in
+      return @@ E_sequence ab'
+  )
+  | E_assignment (s, lrl, exp) -> (
+      let exp' = self exp in
+      if Var.equal s x then raise Bad_argument ;
+      return @@ E_assignment (s, lrl, exp')
+  )
+
+let%expect_test _ =
+  let dummy_type = T_base Base_unit in
+  let wrap e = { content = e ; type_value = dummy_type } in
+
+  let show_subst ~body ~x ~expr =
+    Format.printf "(%a)[%a := %a] =@ %a"
+      PP.expression body
+      Var.pp x
+      PP.expression expr
+      PP.expression (subst_expression ~body ~x ~expr) in
+
+  let x = Var.of_name "x" in
+  let y = Var.of_name "y" in
+  let z = Var.of_name "z" in
+
+  let var x = wrap (E_variable x) in
+  let app f x = wrap (E_application (f, x)) in
+  let lam x u = wrap (E_closure { binder = x ; body = u }) in
+  let unit = wrap (E_literal D_unit) in
+
+  (* substituted var *)
+  Var.reset_counter () ;
+  show_subst
+    ~body:(var x)
+    ~x:x
+    ~expr:unit ;
+  [%expect{|
+    (V(x))[x := L(unit)] =
+    L(unit) |}] ;
+
+  (* other var *)
+  Var.reset_counter () ;
+  show_subst
+    ~body:(var y)
+    ~x:x
+    ~expr:unit ;
+  [%expect{|
+    (V(y))[x := L(unit)] =
+    V(y)
+  |}] ;
+
+  (* closure shadowed *)
+  Var.reset_counter () ;
+  show_subst
+    ~body:(lam x (var x))
+    ~x:x
+    ~expr:unit ;
+  [%expect{|
+    (C(fun x -> (V(x))))[x := L(unit)] =
+    C(fun x -> (V(x)))
+  |}] ;
+
+  (* closure not shadowed *)
+  Var.reset_counter () ;
+  show_subst
+    ~body:(lam y (var x))
+    ~x:x
+    ~expr:unit ;
+  [%expect{|
+    (C(fun y -> (V(x))))[x := L(unit)] =
+    C(fun y -> (L(unit)))
+  |}] ;
+
+  (* closure capture-avoidance *)
+  Var.reset_counter () ;
+  show_subst
+    ~body:(lam y (app (var x) (var y)))
+    ~x:x
+    ~expr:(wrap (E_variable y)) ;
+  [%expect{|
+    (C(fun y -> ((V(x))@(V(y)))))[x := V(y)] =
+    C(fun y#1 -> ((V(y))@(V(y#1))))
+  |}] ;
+
+  (* let-in shadowed (not in rhs) *)
+  Var.reset_counter () ;
+  show_subst
+    ~body:(wrap (E_let_in ((x, dummy_type), var x, var x)))
+    ~x:x
+    ~expr:unit ;
+  [%expect{|
+    (let x = V(x) in ( V(x) ))[x := L(unit)] =
+    let x = L(unit) in ( V(x) )
+  |}] ;
+
+  (* let-in not shadowed *)
+  Var.reset_counter () ;
+  show_subst
+    ~body:(wrap (E_let_in ((y, dummy_type), var x, var x)))
+    ~x:x
+    ~expr:unit ;
+  [%expect{|
+    (let y = V(x) in ( V(x) ))[x := L(unit)] =
+    let y = L(unit) in ( L(unit) )
+  |}] ;
+
+  (* let-in capture avoidance *)
+  Var.reset_counter () ;
+  show_subst
+    ~body:(wrap (E_let_in ((y, dummy_type), var x,
+                           app (var x) (var y))))
+    ~x:x
+    ~expr:(var y) ;
+  [%expect{|
+    (let y = V(x) in ( (V(x))@(V(y)) ))[x := V(y)] =
+    let y#1 = V(y) in ( (V(y))@(V(y#1)) )
+  |}] ;
+
+  (* iter shadowed *)
+  Var.reset_counter () ;
+  show_subst
+    ~body:(wrap (E_iterator ("ITER", ((x , dummy_type) , var x) , var x)))
+    ~x:x
+    ~expr:unit ;
+  [%expect{|
+    (for_ITER x of V(x) do ( V(x) ))[x := L(unit)] =
+    for_ITER x of L(unit) do ( V(x) )
+  |}] ;
+
+  (* iter not shadowed *)
+  Var.reset_counter () ;
+  show_subst
+    ~body:(wrap (E_iterator ("ITER", ((y , dummy_type) , var x) , var x)))
+    ~x:x
+    ~expr:unit ;
+  [%expect{|
+    (for_ITER y of V(x) do ( V(x) ))[x := L(unit)] =
+    for_ITER y of L(unit) do ( L(unit) )
+  |}] ;
+
+  (* iter capture-avoiding *)
+  Var.reset_counter () ;
+  show_subst
+    ~body:(wrap (E_iterator ("ITER", ((y , dummy_type) , app (var x) (var y)), app (var x) (var y))))
+    ~x:x
+    ~expr:(var y) ;
+  [%expect{|
+    (for_ITER y of (V(x))@(V(y)) do ( (V(x))@(V(y)) ))[x := V(y)] =
+    for_ITER y#1 of (V(y))@(V(y)) do ( (V(y))@(V(y#1)) )
+  |}] ;
+
+  (* if_cons shadowed 1 *)
+  Var.reset_counter () ;
+  show_subst
+    ~body:(wrap (E_if_cons (var x,
+                            var x,
+                            (((x, dummy_type), (y, dummy_type)),
+                             var x))))
+    ~x:x
+    ~expr:unit ;
+  [%expect{|
+    (V(x) ?? V(x) : (x :: y) -> V(x))[x := L(unit)] =
+    L(unit) ?? L(unit) : (x :: y) -> V(x)
+  |}] ;
+
+  (* if_cons shadowed 2 *)
+  Var.reset_counter () ;
+  show_subst
+    ~body:(wrap (E_if_cons (var x,
+                            var x,
+                            (((y, dummy_type), (x, dummy_type)),
+                             var x))))
+    ~x:x
+    ~expr:unit ;
+  [%expect{|
+    (V(x) ?? V(x) : (y :: x) -> V(x))[x := L(unit)] =
+    L(unit) ?? L(unit) : (y :: x) -> V(x)
+  |}] ;
+
+  (* if_cons not shadowed *)
+  Var.reset_counter () ;
+  show_subst
+    ~body:(wrap (E_if_cons (var x,
+                            var x,
+                            (((y, dummy_type), (z, dummy_type)),
+                             var x))))
+    ~x:x
+    ~expr:unit ;
+  [%expect{|
+    (V(x) ?? V(x) : (y :: z) -> V(x))[x := L(unit)] =
+    L(unit) ?? L(unit) : (y :: z) -> L(unit)
+  |}] ;
+
+  (* if_cons capture avoidance 1 *)
+  Var.reset_counter () ;
+  show_subst
+    ~body:(wrap (E_if_cons (var x,
+                            var x,
+                            (((y, dummy_type), (z, dummy_type)),
+                             app (var x) (app (var y) (var z))))))
+    ~x:x
+    ~expr:(var y) ;
+  [%expect{|
+    (V(x) ?? V(x) : (y :: z) -> (V(x))@((V(y))@(V(z))))[x := V(y)] =
+    V(y) ?? V(y) : (y#1 :: z) -> (V(y))@((V(y#1))@(V(z)))
+  |}] ;
+
+  (* if_cons capture avoidance 2 *)
+  Var.reset_counter () ;
+  show_subst
+    ~body:(wrap (E_if_cons (var x,
+                            var x,
+                            (((y, dummy_type), (z, dummy_type)),
+                             app (var x) (app (var y) (var z))))))
+    ~x:x
+    ~expr:(var z) ;
+  [%expect{|
+    (V(x) ?? V(x) : (y :: z) -> (V(x))@((V(y))@(V(z))))[x := V(z)] =
+    V(z) ?? V(z) : (y :: z#1) -> (V(z))@((V(y))@(V(z#1)))
+  |}] ;
+
+  (* old bug *)
+  Var.reset_counter () ;
+  let y0 = Var.fresh ~name:"y" () in
+  show_subst
+    ~body:(lam y (lam y0 (app (var x) (app (var y) (var y0)))))
+    ~x:x
+    ~expr:(var y) ;
+  [%expect{|
+    (C(fun y -> (C(fun y#1 -> ((V(x))@((V(y))@(V(y#1))))))))[x := V(y)] =
+    C(fun y#2 -> (C(fun y#1 -> ((V(y))@((V(y#2))@(V(y#1)))))))
+  |}] ;
diff --git a/src/passes/8-compiler/compiler_environment.ml b/src/passes/8-compiler/compiler_environment.ml
index d205c421b..746464d49 100644
--- a/src/passes/8-compiler/compiler_environment.ml
+++ b/src/passes/8-compiler/compiler_environment.ml
@@ -5,12 +5,12 @@ open Michelson
 
 let empty : environment = []
 
-let get : environment -> string -> michelson result = fun e s ->
+let get : environment -> Var.t -> michelson result = fun e s ->
   let%bind (_ , position) =
     let error =
       let title () = "Environment.get" in
-      let content () = Format.asprintf "%s in %a"
-          s PP.environment e in
+      let content () = Format.asprintf "%a in %a"
+          Var.pp s PP.environment e in
       error title content in
     generic_try error @@
     (fun () -> Environment.get_i s e) in
@@ -34,7 +34,7 @@ let get : environment -> string -> michelson result = fun e s ->
 
   ok code
 
-let set : environment -> string -> michelson result = fun e s ->
+let set : environment -> Var.t -> michelson result = fun e s ->
   let%bind (_ , position) =
     generic_try (simple_error "Environment.set") @@
     (fun () -> Environment.get_i s e) in
@@ -65,8 +65,8 @@ let pack_closure : environment -> selector -> michelson result = fun e lst ->
   let e_lst =
     let e_lst = Environment.to_list e in
     let aux selector (s , _) =
-      match List.mem s selector with
-      | true -> List.remove_element s selector , true
+      match List.mem ~compare:Var.compare s selector with
+      | true -> List.remove_element ~compare:Var.compare s selector , true
       | false -> selector , false in
     let e_lst' = List.fold_map_right aux lst e_lst in
     let e_lst'' = List.combine e_lst e_lst' in
diff --git a/src/passes/8-compiler/compiler_environment.mli b/src/passes/8-compiler/compiler_environment.mli
index a82e6e48a..4f167ff9b 100644
--- a/src/passes/8-compiler/compiler_environment.mli
+++ b/src/passes/8-compiler/compiler_environment.mli
@@ -7,8 +7,8 @@ open Michelson
 module Stack = Meta_michelson.Stack
 *)
 val empty: environment
-val get : environment -> string -> michelson result
-val set : environment -> string -> michelson result
+val get : environment -> Var.t -> michelson result
+val set : environment -> Var.t -> michelson result
 
 val pack_closure : environment -> selector -> michelson result
 val unpack_closure : environment -> michelson result
diff --git a/src/passes/8-compiler/compiler_program.ml b/src/passes/8-compiler/compiler_program.ml
index 7bc85aeed..01ddac003 100644
--- a/src/passes/8-compiler/compiler_program.ml
+++ b/src/passes/8-compiler/compiler_program.ml
@@ -457,7 +457,7 @@ let get_main : program -> string -> (anon_function * _) result = fun p entry ->
   let is_main (((name , expr), _):toplevel_statement) =
     match Combinators.Expression.(get_content expr , get_type expr)with
     | (E_closure content , T_function ty)
-      when name = entry ->
+      when Var.equal name (Var.of_name entry) ->
         Some (content , ty)
     | _ ->  None
   in
diff --git a/src/stages/mini_c/PP.ml b/src/stages/mini_c/PP.ml
index c3db61cb5..89b01b8be 100644
--- a/src/stages/mini_c/PP.ml
+++ b/src/stages/mini_c/PP.ml
@@ -42,7 +42,7 @@ and annotated ppf : type_value annotated -> _ = function
   | (None, a) -> type_ ppf a
 
 and environment_element ppf ((s, tv) : environment_element) =
-  Format.fprintf ppf "%s : %a" s type_ tv
+  Format.fprintf ppf "%a : %a" Var.pp s type_ tv
 
 and environment ppf (x:environment) =
   fprintf ppf "Env[%a]" (list_sep_d environment_element) x
@@ -75,7 +75,7 @@ and value_assoc ppf : (value * value) -> unit = fun (a, b) ->
 and expression' ppf (e:expression') = match e with
   | E_skip -> fprintf ppf "skip"
   | E_closure x -> fprintf ppf "C(%a)" function_ x
-  | E_variable v -> fprintf ppf "V(%s)" v
+  | E_variable v -> fprintf ppf "V(%a)" Var.pp v
   | E_application(a, b) -> fprintf ppf "(%a)@(%a)" expression a expression b
   | E_constant(p, lst) -> fprintf ppf "%s %a" p (pp_print_list ~pp_sep:space_sep expression) lst
   | E_literal v -> fprintf ppf "L(%a)" value v
@@ -85,19 +85,25 @@ and expression' ppf (e:expression') = match e with
   | E_make_empty_set _ -> fprintf ppf "set[]"
   | E_make_none _ -> fprintf ppf "none"
   | E_if_bool (c, a, b) -> fprintf ppf "%a ? %a : %a" expression c expression a expression b
-  | E_if_none (c, n, ((name, _) , s)) -> fprintf ppf "%a ?? %a : %s -> %a" expression c expression n name expression s
-  | E_if_cons (c, n, (((hd_name, _) , (tl_name, _)) , cons)) -> fprintf ppf "%a ?? %a : (%s :: %s) -> %a" expression c expression n hd_name tl_name expression cons
+  | E_if_none (c, n, ((name, _) , s)) ->
+    fprintf ppf "%a ?? %a : %a -> %a"
+      expression c expression n Var.pp name expression s
+  | E_if_cons (c, n, (((hd_name, _) , (tl_name, _)) , cons)) ->
+    fprintf ppf "%a ?? %a : (%a :: %a) -> %a"
+      expression c expression n Var.pp hd_name Var.pp tl_name expression cons
   | E_if_left (c, ((name_l, _) , l), ((name_r, _) , r)) ->
-      fprintf ppf "%a ?? %s -> %a : %s -> %a" expression c name_l expression l name_r expression r
+      fprintf ppf "%a ?? %a -> %a : %a -> %a"
+        expression c Var.pp name_l expression l Var.pp name_r expression r
   | E_sequence (a , b) -> fprintf ppf "%a ;; %a" expression a expression b
   | E_let_in ((name , _) , expr , body) ->
-      fprintf ppf "let %s = %a in ( %a )" name expression expr expression body
+      fprintf ppf "let %a = %a in ( %a )" Var.pp name expression expr expression body
   | E_iterator (s , ((name , _) , body) , expr) ->
-      fprintf ppf "for_%s %s of %a do ( %a )" s name expression expr expression body
+      fprintf ppf "for_%s %a of %a do ( %a )" s Var.pp name expression expr expression body
   | E_fold (((name , _) , body) , collection , initial) ->
-      fprintf ppf "fold %a on %a with %s do ( %a )" expression collection expression initial name expression body
+    fprintf ppf "fold %a on %a with %a do ( %a )"
+      expression collection expression initial Var.pp name expression body
   | E_assignment (r , path , e) ->
-      fprintf ppf "%s.%a := %a" r (list_sep lr (const ".")) path expression e
+      fprintf ppf "%a.%a := %a" Var.pp r (list_sep lr (const ".")) path expression e
   | E_while (e , b) ->
       fprintf ppf "while (%a) %a" expression e expression b
 
@@ -110,15 +116,28 @@ and expression_with_type : _ -> expression -> _  = fun ppf e ->
     type_ e.type_value
 
 and function_ ppf ({binder ; body}:anon_function) =
-  fprintf ppf "fun %s -> (%a)"
-    binder
+  fprintf ppf "fun %a -> (%a)"
+    Var.pp binder
     expression body
 
-and assignment ppf ((n, e):assignment) = fprintf ppf "%s = %a;" n expression e
+and assignment ppf ((n, e):assignment) = fprintf ppf "%a = %a;" Var.pp n expression e
 
-and declaration ppf ((n, e):assignment) = fprintf ppf "let %s = %a;" n expression e
+and declaration ppf ((n, e):assignment) = fprintf ppf "let %a = %a;" Var.pp n expression e
 
 let tl_statement ppf (ass, _) = assignment ppf ass
 
 let program ppf (p:program) =
   fprintf ppf "Program:\n---\n%a" (pp_print_list ~pp_sep:pp_print_newline tl_statement) p
+
+let%expect_test _ =
+  let pp = expression' Format.std_formatter in
+  let dummy_type = T_base Base_unit in
+  let wrap e = { content = e ; type_value = dummy_type } in
+  pp @@ E_closure { binder = Var.of_name "y" ; body = wrap (E_variable (Var.of_name "y")) } ;
+  [%expect{|
+    C(fun y -> (V(y)))
+  |}] ;
+  pp @@ E_closure { binder = Var.of_name "z" ; body = wrap (E_variable (Var.of_name "z")) } ;
+  [%expect{|
+    C(fun z -> (V(z)))
+  |}]
diff --git a/src/stages/mini_c/combinators.ml b/src/stages/mini_c/combinators.ml
index 556682907..66a98c855 100644
--- a/src/stages/mini_c/combinators.ml
+++ b/src/stages/mini_c/combinators.ml
@@ -168,13 +168,6 @@ let t_function x y : type_value = T_function ( x , y )
 let t_pair x y : type_value = T_pair ( x , y )
 let t_union x y : type_value = T_or ( x , y )
 
-let quote binder body : anon_function =
-  {
-    binder ;
-    body ;
-  }
-
-
 let e_int expr : expression = Expression.make_tpl (expr, t_int)
 let e_unit : expression = Expression.make_tpl (E_literal D_unit, t_unit)
 let e_skip : expression = Expression.make_tpl (E_skip, t_unit)
@@ -188,13 +181,6 @@ let ez_e_sequence a b : expression = Expression.(make_tpl (E_sequence (make_tpl
 
 let d_unit : value = D_unit
 
-let basic_quote expr in_ty out_ty : expression result =
-  let expr' = E_closure (quote "input" expr) in
-  ok @@ Expression.make_tpl (expr' , t_function in_ty out_ty)
-
-let basic_int_quote expr : expression result =
-  basic_quote expr t_int t_int
-
 
 let environment_wrap pre_environment post_environment = { pre_environment ; post_environment }
 let id_environment_wrap e = environment_wrap e e
diff --git a/src/stages/mini_c/combinators.mli b/src/stages/mini_c/combinators.mli
index f686bd522..78b00212f 100644
--- a/src/stages/mini_c/combinators.mli
+++ b/src/stages/mini_c/combinators.mli
@@ -66,18 +66,14 @@ val e_int : Expression.t' -> Expression.t
 *)
 val e_unit : Expression.t
 val e_skip : Expression.t
-val e_var_int : string -> Expression.t
-val e_let_in : string -> type_value -> Expression.t -> Expression.t -> Expression.t
+val e_var_int : Var.t -> Expression.t
+val e_let_in : Var.t -> type_value -> Expression.t -> Expression.t -> Expression.t
 
 val ez_e_sequence : Expression.t' -> Expression.t -> expression
 (*
 val ez_e_return : Expression.t -> Expression.t
 *)
 val d_unit : value
-(*
-val basic_quote : type_value -> type_value -> Expression.t -> anon_function result
-*)
-val basic_int_quote : expression -> expression result
 
 val environment_wrap : environment -> environment -> environment_wrap
 val id_environment_wrap : environment -> environment_wrap
diff --git a/src/stages/mini_c/combinators_smart.ml b/src/stages/mini_c/combinators_smart.ml
deleted file mode 100644
index 6cffd7226..000000000
--- a/src/stages/mini_c/combinators_smart.ml
+++ /dev/null
@@ -1,6 +0,0 @@
-open Types
-open Combinators
-
-let basic_int_quote_env : environment =
-  let e = Environment.empty in
-  Environment.add ("input", t_int) e
diff --git a/src/stages/mini_c/combinators_smart.mli b/src/stages/mini_c/combinators_smart.mli
deleted file mode 100644
index 68ff160f2..000000000
--- a/src/stages/mini_c/combinators_smart.mli
+++ /dev/null
@@ -1,3 +0,0 @@
-open Types
-
-val basic_int_quote_env : environment
diff --git a/src/stages/mini_c/dune b/src/stages/mini_c/dune
index d7e69d219..a4bf61bcb 100644
--- a/src/stages/mini_c/dune
+++ b/src/stages/mini_c/dune
@@ -5,8 +5,7 @@
     simple-utils
     tezos-utils
   )
-  (preprocess
-    (pps ppx_let)
-  )
+  (inline_tests)
+  (preprocess (pps ppx_expect ppx_let))
   (flags (:standard -w +1..62-4-9-44-40-42-48-30@39@33 -open Simple_utils ))
 )
diff --git a/src/stages/mini_c/environment.ml b/src/stages/mini_c/environment.ml
index 8b4bb2924..9cd48faaa 100644
--- a/src/stages/mini_c/environment.ml
+++ b/src/stages/mini_c/environment.ml
@@ -21,23 +21,23 @@ module Environment (* : ENVIRONMENT *) = struct
   let empty : t = []
   let add : element -> t -> t  = List.cons
   let concat : t list -> t  = List.concat
-  let get_opt : string -> t -> type_value option  = List.assoc_opt
-  let has : string -> t -> bool = fun s t ->
+  let get_opt : Var.t -> t -> type_value option  = List.assoc_opt ~compare:Var.compare
+  let has : Var.t -> t -> bool = fun s t ->
     match get_opt s t with
     | None -> false
     | Some _ -> true
-  let get_i : string -> t -> (type_value * int) = List.assoc_i
+  let get_i : Var.t -> t -> (type_value * int) = List.assoc_i ~compare:Var.compare
   let of_list : element list -> t = fun x -> x
   let to_list : t -> element list = fun x -> x
-  let get_names : t -> string list = List.map fst
+  let get_names : t -> Var.t list = List.map fst
   let remove : int -> t -> t = List.remove
 
-  let select ?(rev = false) ?(keep = true) : string list -> t -> t = fun lst env ->
+  let select ?(rev = false) ?(keep = true) : Var.t list -> t -> t = fun lst env ->
     let e_lst =
       let e_lst = to_list env in
       let aux selector (s , _) =
-        match List.mem s selector with
-        | true -> List.remove_element s selector , keep
+        match List.mem ~compare:Var.compare s selector with
+        | true -> List.remove_element ~compare:Var.compare s selector , keep
         | false -> selector , not keep in
       let e_lst' =
         if rev = keep
diff --git a/src/stages/mini_c/environment.mli b/src/stages/mini_c/environment.mli
index a9ac6afef..19ae53b70 100644
--- a/src/stages/mini_c/environment.mli
+++ b/src/stages/mini_c/environment.mli
@@ -11,15 +11,15 @@ module Environment : sig
   val add : element -> t -> t
   val concat : t list -> t
   (*
-  val get_opt : string -> t -> type_value option
-  val has : string -> t -> bool
+  val get_opt : Var.t -> t -> type_value option
+  val has : Var.t -> t -> bool
   *)
-  val get_i : string -> t -> (type_value * int)
+  val get_i : Var.t -> t -> (type_value * int)
   val of_list : element list -> t
   val to_list : t -> element list
-  val get_names : t -> string list
+  val get_names : t -> Var.t list
   val remove : int -> t -> t
-  val select : ?rev:bool -> ?keep:bool -> string list -> t -> t
+  val select : ?rev:bool -> ?keep:bool -> Var.t list -> t -> t
   (*
   val fold : ('a -> element -> 'a ) -> 'a -> t -> 'a
   val filter : ( element -> bool ) -> t -> t
@@ -36,20 +36,20 @@ val empty : t
 val add : element -> t -> t
 val concat : t list -> t
 (*
-val get_opt : string -> t -> type_value option
+val get_opt : Var.t -> t -> type_value option
 *)
-val has : string -> t -> bool
+val has : Var.t -> t -> bool
 (*
-val get_i : string -> t -> (type_value * int)
+val get_i : Var.t -> t -> (type_value * int)
 *)
 val of_list : element list -> t
 (*
 val to_list : t -> element list
-val get_names : t -> string list
+val get_names : t -> Var.t list
 val remove : int -> t -> t
 
 *)
-val select : ?rev:bool -> ?keep:bool -> string list -> t -> t
+val select : ?rev:bool -> ?keep:bool -> Var.t list -> t -> t
 val fold : ('a -> element -> 'a ) -> 'a -> t -> 'a
 val filter : ( element -> bool ) -> t -> t
 
diff --git a/src/stages/mini_c/misc.ml b/src/stages/mini_c/misc.ml
index 90f9bb2eb..578c3cfcf 100644
--- a/src/stages/mini_c/misc.ml
+++ b/src/stages/mini_c/misc.ml
@@ -24,13 +24,16 @@ end
 
 module Free_variables = struct
 
-  type bindings = string list
-  let mem : string -> bindings -> bool = List.mem
-  let singleton : string -> bindings = fun s -> [ s ]
+  type bindings = Var.t list
+  let mem : Var.t -> bindings -> bool = List.memq ~eq:Var.equal
+  let mem_count : Var.t -> bindings -> int =
+    fun x fvs ->
+    List.length (List.filter (Var.equal x) fvs)
+  let singleton : Var.t -> bindings = fun s -> [ s ]
   let union : bindings -> bindings -> bindings = (@)
   let unions : bindings list -> bindings = List.concat
   let empty : bindings = []
-  let of_list : string list -> bindings = fun x -> x
+  let of_list : Var.t list -> bindings = fun x -> x
 
   let rec expression : bindings -> expression -> bindings = fun b e ->
     let self = expression b in
@@ -121,7 +124,7 @@ end
    Converts `expr` in `fun () -> expr`.
 *)
 let functionalize (body : expression) : expression =
-  let content = E_closure { binder = "_" ; body } in
+  let content = E_closure { binder = Var.fresh () ; body } in
   let type_value = t_function t_unit body.type_value in
   { content ; type_value }
 
@@ -130,7 +133,7 @@ let get_entry (lst : program) (name : string) : (expression * int) result =
     trace_option (Errors.missing_entry_point name) @@
     let aux x =
       let (((decl_name , decl_expr) , _)) = x in
-      if (decl_name = name)
+      if (Var.equal decl_name (Var.of_name name))
       then Some decl_expr
       else None
     in
@@ -139,7 +142,7 @@ let get_entry (lst : program) (name : string) : (expression * int) result =
   let entry_index =
     let aux x =
       let (((decl_name , _) , _)) = x in
-      decl_name = name
+      Var.equal decl_name (Var.of_name name)
     in
     List.find_index aux lst
   in
diff --git a/src/stages/mini_c/types.ml b/src/stages/mini_c/types.ml
index ec4f043e3..8c599e146 100644
--- a/src/stages/mini_c/types.ml
+++ b/src/stages/mini_c/types.ml
@@ -23,7 +23,7 @@ type type_value =
   | T_contract of type_value
   | T_option of type_value
 
-and environment_element = string * type_value
+and environment_element = Var.t * type_value
 
 and environment = environment_element list
 
@@ -32,8 +32,8 @@ type environment_wrap = {
   post_environment : environment ;
 }
 
-type var_name = string
-type fun_name = string
+type var_name = Var.t
+type fun_name = Var.t
 
 type value =
   | D_unit
@@ -78,7 +78,7 @@ and expression' =
   | E_if_left of expression * ((var_name * type_value) * expression) * ((var_name * type_value) * expression)
   | E_let_in of ((var_name * type_value) * expression * expression)
   | E_sequence of (expression * expression)
-  | E_assignment of (string * [`Left | `Right] list * expression)
+  | E_assignment of (var_name * [`Left | `Right] list * expression)
   | E_while of (expression * expression)
 
 and expression = {
@@ -91,7 +91,7 @@ and assignment = var_name * expression
 and toplevel_statement = assignment * environment_wrap
 
 and anon_function = {
-  binder : string ;
+  binder : var_name ;
   body : expression ;
 }
 
diff --git a/vendors/ligo-utils/simple-utils/simple_utils.ml b/vendors/ligo-utils/simple-utils/simple_utils.ml
index 0b23509bd..1db630bb7 100644
--- a/vendors/ligo-utils/simple-utils/simple_utils.ml
+++ b/vendors/ligo-utils/simple-utils/simple_utils.ml
@@ -6,10 +6,12 @@ module Location = Location
 
 module List = X_list
 module Option = X_option
+module Int = X_int
 module Tuple = Tuple
 module Map = X_map
 module Dictionary = Dictionary
 module Tree = Tree
 module Region = Region
 module Pos = Pos
+module Var = Var
 
diff --git a/vendors/ligo-utils/simple-utils/tuple.ml b/vendors/ligo-utils/simple-utils/tuple.ml
index ad451e74d..5773f86dd 100644
--- a/vendors/ligo-utils/simple-utils/tuple.ml
+++ b/vendors/ligo-utils/simple-utils/tuple.ml
@@ -1,5 +1,6 @@
 let map_h_2 f g (a , b) = (f a , g b)
 let map2 f (a, b) = (f a, f b)
+let map3 f (a , b , c) = (f a , f b , f c)
 let apply2 f (a, b) = f a b
 let list2 (a, b) = [a;b]
 
diff --git a/vendors/ligo-utils/simple-utils/var.ml b/vendors/ligo-utils/simple-utils/var.ml
new file mode 100644
index 000000000..9af624e56
--- /dev/null
+++ b/vendors/ligo-utils/simple-utils/var.ml
@@ -0,0 +1,39 @@
+type t = {
+  name : string ;
+  counter : int option ;
+}
+
+let pp ppf v =
+  match v.counter with
+  | None -> Format.fprintf ppf "%s" v.name
+  | Some i -> Format.fprintf ppf "%s#%d" v.name i
+
+module Int = X_int
+module Option = X_option
+
+let equal v1 v2 =
+  String.equal v1.name v2.name
+  && Option.equal Int.equal v1.counter v2.counter
+
+let compare v1 v2 =
+  let cname = String.compare v1.name v2.name in
+  if Int.equal cname 0
+  then Option.compare Int.compare v1.counter v2.counter
+  else cname
+
+let global_counter = ref 0
+
+let reset_counter () = global_counter := 0
+
+let of_name name =
+  { name = name ;
+    counter = None
+  }
+
+let fresh ?name () =
+  let name = Option.unopt ~default:"" name in
+  let counter = incr global_counter ; Some !global_counter in
+  { name ; counter }
+
+let fresh_like v =
+  fresh ~name:v.name ()
diff --git a/vendors/ligo-utils/simple-utils/var.mli b/vendors/ligo-utils/simple-utils/var.mli
new file mode 100644
index 000000000..8d8528298
--- /dev/null
+++ b/vendors/ligo-utils/simple-utils/var.mli
@@ -0,0 +1,42 @@
+(* Currently, Var.t is equivalent to (string * int option). The
+   optional counter value is present on variables generated with
+   `fresh`.
+
+   The intent is that there are two disjoint classes of variables:
+   'user variables' (embedded with `of_name`) and 'generated
+   variables' (generated with `fresh`.)
+
+   Vars with indices are printed as %s#%d. This could be confusing if
+   vars like `name_of "foo#121"` are allowed -- `name_of "foo#121"`
+   will be _not equal_ to a generated var `fresh ~name:"foo"` with
+   counter 121, despite being printed the same way.
+
+   This module does not prevent that confusion. But, the LIGO lexer
+   does not accept names like "foo#121" as possible variable names, so
+   this confusion should not arise for us.  *)
+
+type t
+
+val equal : t -> t -> bool
+val compare : t -> t -> int
+
+(* Prints vars as %s or %s#%d *)
+val pp : Format.formatter -> t -> unit
+
+(* Construct a user variable directly from a string. This should only
+   be used for embedding user variable names. For programmatically
+   generated variables, use `fresh`. Take care not to cause
+   shadowing/capture except as the user intended. *)
+val of_name : string -> t
+
+(* Generate a variable, using a counter value from a _global_
+   counter. If the name is not provided, it will be empty. *)
+val fresh : ?name:string -> unit -> t
+
+(* Generate a variable as with `fresh`, reusing the name part of the
+   given variable. *)
+val fresh_like : t -> t
+
+(* Reset the global counter. Danger, do not use... Provided for tests
+   only. *)
+val reset_counter : unit -> unit
diff --git a/vendors/ligo-utils/simple-utils/x_int.ml b/vendors/ligo-utils/simple-utils/x_int.ml
new file mode 100644
index 000000000..818267d10
--- /dev/null
+++ b/vendors/ligo-utils/simple-utils/x_int.ml
@@ -0,0 +1,2 @@
+let equal : int -> int -> bool = (=)
+let compare : int -> int -> int = compare
diff --git a/vendors/ligo-utils/simple-utils/x_list.ml b/vendors/ligo-utils/simple-utils/x_list.ml
index a7d36261b..7c856146e 100644
--- a/vendors/ligo-utils/simple-utils/x_list.ml
+++ b/vendors/ligo-utils/simple-utils/x_list.ml
@@ -39,11 +39,17 @@ let fold_map : type acc ele ret . (acc -> ele -> (acc * ret)) -> acc -> ele list
 
 let fold_right' f init lst = List.fold_left f init (List.rev lst)
 
-let rec remove_element x lst =
+(* breaking a dependency cycle with X_option *)
+let unopt ~default x = match x with
+  | None -> default
+  | Some x -> x
+
+let rec remove_element ?compare:cmp x lst =
+  let compare = unopt ~default:compare cmp in
   match lst with
   | [] -> raise (Failure "X_list.remove_element")
-  | hd :: tl when x = hd -> tl
-  | hd :: tl -> hd :: remove_element x tl
+  | hd :: tl when compare x hd = 0 -> tl
+  | hd :: tl -> hd :: remove_element ~compare x tl
 
 let filter_map f =
   let rec aux acc lst = match lst with
@@ -94,10 +100,10 @@ let find_full f lst =
   | _ :: tl -> aux (n + 1) tl in
   aux 0 lst
 
-let assoc_i x lst =
+let assoc_i ~compare x lst =
   let rec aux n = function
     | [] -> raise (Failure "List:assoc_i")
-    | (x', y) :: _ when x = x' -> (y, n)
+    | (x', y) :: _ when compare x x' = 0 -> (y, n)
     | _ :: tl -> aux (n + 1) tl
   in
   aux 0 lst
@@ -139,6 +145,35 @@ let to_singleton = function
   | [a] -> Some a
   | _ -> None
 
+
+(** overriding stdlib List functions with optional compare/eq
+   arguments *)
+
+let rec mem ?compare:cmp x =
+  let compare = unopt ~default:compare cmp in
+  function
+  | [] -> false
+  | a::l -> compare a x = 0 || mem ~compare x l
+
+let rec memq ?eq:eq x =
+  let eq = unopt ~default:(=) eq in
+  function
+  | [] -> false
+  | a::l -> eq a x || memq ~eq x l
+
+let rec assoc ?compare:cmp x =
+  let compare = unopt ~default:compare cmp in
+  function
+    [] -> raise Not_found
+  | (a,b)::l -> if compare a x = 0 then b else assoc ~compare x l
+
+let rec assoc_opt ?compare:cmp x =
+  let compare = unopt ~default:compare cmp in
+  function
+    [] -> None
+  | (a,b)::l -> if compare a x = 0 then Some b else assoc_opt ~compare x l
+
+
 module Ne = struct
 
   type 'a t = 'a * 'a list
diff --git a/vendors/ligo-utils/simple-utils/x_option.ml b/vendors/ligo-utils/simple-utils/x_option.ml
index ad69d5303..77096546f 100644
--- a/vendors/ligo-utils/simple-utils/x_option.ml
+++ b/vendors/ligo-utils/simple-utils/x_option.ml
@@ -72,3 +72,16 @@ let bind_smap (s:_ X_map.String.t) =
   fold aux s (Some empty)
 
 let bind_map_smap f smap = bind_smap (X_map.String.map f smap)
+
+let equal eq x y =
+  match (x, y) with
+  | (None, None) -> true
+  | (Some x, Some y) -> eq x y
+  | _ -> false
+
+let compare compare x y =
+  match (x, y) with
+  | (None, None) -> 0
+  | (None, Some _) -> -1
+  | (Some _, None) -> 1
+  | (Some x, Some y) -> compare x y