diff --git a/plutus-core/plutus-core.cabal b/plutus-core/plutus-core.cabal
index 956d3ade95c..6dd100edf8b 100644
--- a/plutus-core/plutus-core.cabal
+++ b/plutus-core/plutus-core.cabal
@@ -240,6 +240,7 @@ library
     PlutusCore.Builtin.KnownKind
     PlutusCore.Builtin.KnownType
     PlutusCore.Builtin.KnownTypeAst
+    PlutusCore.Builtin.Let
     PlutusCore.Builtin.Meaning
     PlutusCore.Builtin.Polymorphism
     PlutusCore.Builtin.Result
diff --git a/plutus-core/plutus-core/src/PlutusCore/Builtin.hs b/plutus-core/plutus-core/src/PlutusCore/Builtin.hs
index f95c0427f6d..ee0098a5dd6 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Builtin.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Builtin.hs
@@ -9,6 +9,7 @@ import PlutusCore.Builtin.HasConstant as Export
 import PlutusCore.Builtin.KnownKind as Export
 import PlutusCore.Builtin.KnownType as Export
 import PlutusCore.Builtin.KnownTypeAst as Export
+import PlutusCore.Builtin.Let as Export
 import PlutusCore.Builtin.Meaning as Export
 import PlutusCore.Builtin.Polymorphism as Export
 import PlutusCore.Builtin.Result as Export
diff --git a/plutus-core/plutus-core/src/PlutusCore/Builtin/Let.hs b/plutus-core/plutus-core/src/PlutusCore/Builtin/Let.hs
new file mode 100644
index 00000000000..2645548c7e7
--- /dev/null
+++ b/plutus-core/plutus-core/src/PlutusCore/Builtin/Let.hs
@@ -0,0 +1,45 @@
+{-# LANGUAGE DataKinds         #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RankNTypes        #-}
+{-# LANGUAGE TypeOperators     #-}
+
+module PlutusCore.Builtin.Let where
+
+import PlutusCore.Builtin.KnownType (Spine)
+import PlutusCore.Core.Type (Type, UniOf)
+import PlutusCore.Name.Unique (TyName)
+
+import Control.DeepSeq (NFData (..), rwhnf)
+import Data.Default.Class (Default (..))
+import Data.Text (Text)
+import Data.Vector (Vector)
+import NoThunks.Class
+import Text.PrettyBy (display)
+import Universe
+
+
+class LetBuiltin uni where
+    -- | Given a constant with its type tag and a vector of branches, choose the appropriate branch
+    -- or fail if the constant doesn't correspond to any of the branches (or casing on constants of
+    -- this type isn't supported at all).
+    letBuiltin
+        :: Some (ValueOf uni)
+        -> Either Text [Some (ValueOf uni)]
+
+data LeterBuiltin uni = LeterBuiltin
+    { unLeterBuiltin :: !(Some (ValueOf uni) -> Either Text [Some (ValueOf uni)])
+    }
+
+instance NFData (LeterBuiltin uni) where
+    rnf = rwhnf
+
+deriving via OnlyCheckWhnfNamed "PlutusCore.Builtin.Case.LeterBuiltin" (LeterBuiltin uni)
+    instance NoThunks (LeterBuiltin uni)
+
+instance LetBuiltin uni => Default (LeterBuiltin uni) where
+    def = LeterBuiltin letBuiltin
+
+unavailableLeterBuiltin :: Int -> LeterBuiltin uni
+unavailableLeterBuiltin ver =
+    LeterBuiltin $ \_ -> Left $
+        "'let' TODO " <> display ver
diff --git a/plutus-core/plutus-core/src/PlutusCore/Default/Universe.hs b/plutus-core/plutus-core/src/PlutusCore/Default/Universe.hs
index 1cb022be55f..67e124408e6 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Default/Universe.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Default/Universe.hs
@@ -50,7 +50,7 @@ import PlutusCore.Core.Type (Type (..))
 import PlutusCore.Crypto.BLS12_381.G1 qualified as BLS12_381.G1
 import PlutusCore.Crypto.BLS12_381.G2 qualified as BLS12_381.G2
 import PlutusCore.Crypto.BLS12_381.Pairing qualified as BLS12_381.Pairing
-import PlutusCore.Data (Data)
+import PlutusCore.Data (Data (Constr))
 import PlutusCore.Evaluation.Machine.ExMemoryUsage (IntegerCostedLiterally (..),
                                                     NumBytesCostedAsNumWords (..))
 import PlutusCore.Pretty.Extra (juxtRenderContext)
@@ -651,11 +651,28 @@ instance CaseBuiltin DefaultUni where
               case x of
                 (l, r) -> Right $ headSpine (branches Vector.! 0) [someValueOf tyL l, someValueOf tyR r]
             | otherwise -> Left $ outOfBoundsErr someVal branches
+        DefaultUniData ->
+          case x of
+            Constr ix ds
+              | 0 <= ix && ix < toInteger len ->
+                Right $
+                  headSpine
+                    (branches Vector.! (fromIntegral ix))
+                    (someValueOf DefaultUniData <$> ds)
+              | otherwise -> Left $ outOfBoundsErr someVal branches
+            _ -> Left "Only 'Constr' constructor can be cased"
         _ -> Left $ display uni <> " isn't supported in 'case'"
       where
         !len = Vector.length branches
     {-# INLINE caseBuiltin #-}
 
+instance LetBuiltin DefaultUni where
+  letBuiltin _someVal@(Some (ValueOf uni x)) =
+    case uni of
+      DefaultUniList ty      -> Right $ someValueOf ty <$> x
+      DefaultUniPair tyL tyR -> Right [someValueOf tyL $ fst x, someValueOf tyR $ snd x]
+      _                      -> Left $ display uni <> "no"
+
 {- Note [Stable encoding of tags]
 'encodeUni' and 'decodeUni' are used for serialisation and deserialisation of types from the
 universe and we need serialised things to be extremely stable, hence the definitions of 'encodeUni'
diff --git a/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/ExBudgetingDefaults.hs b/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/ExBudgetingDefaults.hs
index b70266cb250..5c146d6f40d 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/ExBudgetingDefaults.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/ExBudgetingDefaults.hs
@@ -149,19 +149,19 @@ faster than the used in production. Also see Note [noinline for saving on
 ticks]. -}
 defaultCekParametersA :: Typeable ann => MachineParameters CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun ann)
 defaultCekParametersA =
-    MachineParameters def $
+    MachineParameters def def $
         noinline mkMachineVariantParameters DefaultFunSemanticsVariantA cekCostModelVariantA
 
 -- See Note [No inlining for MachineParameters]
 defaultCekParametersB :: Typeable ann => MachineParameters CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun ann)
 defaultCekParametersB =
-    MachineParameters def $
+    MachineParameters def def $
         noinline mkMachineVariantParameters DefaultFunSemanticsVariantB cekCostModelVariantB
 
 -- See Note [No inlining for MachineParameters]
 defaultCekParametersC :: Typeable ann => MachineParameters CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun ann)
 defaultCekParametersC =
-    MachineParameters def $
+    MachineParameters def def $
         noinline mkMachineVariantParameters DefaultFunSemanticsVariantC cekCostModelVariantC
 
 {- Note [noinline for saving on ticks]
@@ -360,6 +360,6 @@ unitCostBuiltinCostModel = BuiltinCostModelBase
 unitCekParameters :: Typeable ann => MachineParameters CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun ann)
 unitCekParameters =
     -- See Note [noinline for saving on ticks].
-    MachineParameters def $
+    MachineParameters def def $
         noinline mkMachineVariantParameters def $
             CostModel unitCekMachineCosts unitCostBuiltinCostModel
diff --git a/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/MachineParameters.hs b/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/MachineParameters.hs
index 948196cd786..6423c2ef3b2 100644
--- a/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/MachineParameters.hs
+++ b/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/MachineParameters.hs
@@ -55,6 +55,7 @@ The @val@ type will be 'CekValue' when we're using this with the CEK machine.
 data MachineParameters machineCosts fun val =
     MachineParameters {
       machineCaserBuiltin      :: CaserBuiltin (UniOf val)
+    , machineLeterBuiltin      :: LeterBuiltin (UniOf val)
     , machineVariantParameters :: MachineVariantParameters machineCosts fun val
     }
     deriving stock Generic
@@ -67,8 +68,8 @@ instance (NoThunks machinecosts, Bounded fun, Enum fun) => NoThunks (MachineVari
       allNoThunks [ noThunks ctx costs, noThunks ctx runtime ]
 
 instance (NoThunks machinecosts, Bounded fun, Enum fun) => NoThunks (MachineParameters machinecosts fun val) where
-  wNoThunks ctx (MachineParameters caser varPars) =
-      allNoThunks [ noThunks ctx caser, noThunks ctx varPars ]
+  wNoThunks ctx (MachineParameters caser leter varPars) =
+      allNoThunks [ noThunks ctx caser, noThunks ctx leter, noThunks ctx varPars ]
 
 {- Note [The CostingPart constraint in mkMachineVariantParameters]
 Discharging the @CostingPart uni fun ~ builtincosts@ constraint in 'mkMachineParameters' causes GHC
diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Analysis/Definitions.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Analysis/Definitions.hs
index 343f2070244..7f2f65209a6 100644
--- a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Analysis/Definitions.hs
+++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Analysis/Definitions.hs
@@ -16,6 +16,7 @@ import PlutusCore.Name.Unique (HasUnique, TermUnique (TermUnique), Unique (Uniqu
 import Control.Lens (forMOf_)
 import Control.Monad.State (MonadState, execStateT)
 import Control.Monad.Writer (MonadWriter, WriterT (runWriterT))
+import Data.Foldable (traverse_)
 
 -- | Given a UPLC term, add all of its term definitions and usages, including its subterms,
 -- to a global map.
@@ -40,6 +41,8 @@ handleTerm = \case
         addUsage n ann TermScope
     LamAbs ann n _ ->
         addDef n ann TermScope
+    Let ann ns _ ->
+        traverse_ (\n -> addDef n ann TermScope) ns
     _               -> pure ()
 
 runTermDefs
diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Instance/Flat.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Instance/Flat.hs
index 1510a708cc7..d07d07d4b5f 100644
--- a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Instance/Flat.hs
+++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Instance/Flat.hs
@@ -65,7 +65,7 @@ tags and their used/available encoding possibilities.
 | Data type        | Function          | Bit Width | Total | Used | Remaining |
 |------------------|-------------------|-----------|-------|------|-----------|
 | default builtins | encodeBuiltin     | 7         | 128   | 54   | 74        |
-| Terms            | encodeTerm        | 4         | 16    | 10   | 6         |
+| Terms            | encodeTerm        | 4         | 16    | 10   | 4         |
 
 For format stability we are manually assigning the tag values to the
 constructors (and we do not use a generic algorithm that may change this order).
@@ -114,16 +114,18 @@ encodeTerm
     => Term name uni fun ann
     -> Encoding
 encodeTerm = \case
-    Var      ann n      -> encodeTermTag 0 <> encode ann <> encode n
-    Delay    ann t      -> encodeTermTag 1 <> encode ann <> encodeTerm t
-    LamAbs   ann n t    -> encodeTermTag 2 <> encode ann <> encode (Binder n) <> encodeTerm t
-    Apply    ann t t'   -> encodeTermTag 3 <> encode ann <> encodeTerm t <> encodeTerm t'
-    Constant ann c      -> encodeTermTag 4 <> encode ann <> encode c
-    Force    ann t      -> encodeTermTag 5 <> encode ann <> encodeTerm t
-    Error    ann        -> encodeTermTag 6 <> encode ann
-    Builtin  ann bn     -> encodeTermTag 7 <> encode ann <> encode bn
-    Constr   ann i es   -> encodeTermTag 8 <> encode ann <> encode i <> encodeListWith encodeTerm es
-    Case     ann arg cs -> encodeTermTag 9 <> encode ann <> encodeTerm arg <> encodeListWith encodeTerm (V.toList cs)
+    Var      ann n      -> encodeTermTag 0  <> encode ann <> encode n
+    Delay    ann t      -> encodeTermTag 1  <> encode ann <> encodeTerm t
+    LamAbs   ann n t    -> encodeTermTag 2  <> encode ann <> encode (Binder n) <> encodeTerm t
+    Apply    ann t t'   -> encodeTermTag 3  <> encode ann <> encodeTerm t <> encodeTerm t'
+    Constant ann c      -> encodeTermTag 4  <> encode ann <> encode c
+    Force    ann t      -> encodeTermTag 5  <> encode ann <> encodeTerm t
+    Error    ann        -> encodeTermTag 6  <> encode ann
+    Builtin  ann bn     -> encodeTermTag 7  <> encode ann <> encode bn
+    Constr   ann i es   -> encodeTermTag 8  <> encode ann <> encode i <> encodeListWith encodeTerm es
+    Case     ann arg cs -> encodeTermTag 9  <> encode ann <> encodeTerm arg <> encodeListWith encodeTerm (V.toList cs)
+    Let      ann ns t   -> encodeTermTag 10 <> encode ann <> encode ns <> encodeTerm t
+    Bind     ann t bs   -> encodeTermTag 11 <> encode ann <> encodeTerm t <> encodeListWith encodeTerm bs
 
 decodeTerm
     :: forall name uni fun ann
@@ -161,6 +163,12 @@ decodeTerm version builtinPred = go
         handleTerm 9 = do
             unless (version >= PLC.plcVersion110) $ fail $ "'case' is not allowed before version 1.1.0, this program has version: " ++ (show $ pretty version)
             Case     <$> decode <*> go <*> (V.fromList <$> decodeListWith go)
+        handleTerm 10 = do
+            -- TODO: fail when version is low
+            Let <$> decode <*> decode <*> go
+        handleTerm 11 = do
+            -- TODO: fail when version is low
+            Bind <$> decode <*> go <*> decodeListWith go
         handleTerm t = fail $ "Unknown term constructor tag: " ++ show t
 
 sizeTerm
@@ -189,6 +197,8 @@ sizeTerm tm sz =
     Builtin  ann bn     -> size ann $ size bn sz'
     Constr   ann i es   -> size ann $ size i $ sizeListWith sizeTerm es sz'
     Case     ann arg cs -> size ann $ sizeTerm arg $ sizeListWith sizeTerm (V.toList cs) sz'
+    Let      ann ns t   -> size ann $ size ns $ sizeTerm t sz'
+    Bind     ann t bs   -> size ann $ sizeTerm t $ sizeListWith sizeTerm bs sz'
 
 -- | An encoder for programs.
 --
diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Instance/Pretty/Classic.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Instance/Pretty/Classic.hs
index 0373e323608..074a95076af 100644
--- a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Instance/Pretty/Classic.hs
+++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Instance/Pretty/Classic.hs
@@ -50,6 +50,14 @@ instance (PrettyClassicBy configName name, PrettyUni uni, Pretty fun, Pretty ann
         Case ann arg cs ->
             sexp "case" (consAnnIf config ann
                 (prettyBy config arg : fmap (prettyBy config) (toList cs)))
+        Let ann names body ->
+          sexp "let" (consAnnIf config ann
+              [ parens' (sep $ prettyBy config <$> names)
+              , prettyBy config body
+              ])
+        Bind ann t binds ->
+          sexp "bind" (consAnnIf config ann
+              (prettyBy config t : (prettyBy config <$> binds)))
       where
         prettyTypeOf :: Some (ValueOf uni) -> Doc dann
         prettyTypeOf (Some (ValueOf uni _ )) = prettyBy juxtRenderContext $ SomeTypeIn uni
diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Instance/Pretty/Readable.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Instance/Pretty/Readable.hs
index 681d1c81ea6..d05b57da726 100644
--- a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Instance/Pretty/Readable.hs
+++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Instance/Pretty/Readable.hs
@@ -12,6 +12,7 @@ module UntypedPlutusCore.Core.Instance.Pretty.Readable () where
 import PlutusCore.Pretty.PrettyConst
 import PlutusCore.Pretty.Readable
 import PlutusPrelude
+import Prettyprinter.Custom (parens')
 import UntypedPlutusCore.Core.Type
 
 import Prettyprinter
@@ -53,6 +54,10 @@ instance
     Constr _ i es -> iterAppDocM $ \_ prettyArg ->
       ("constr" <+> prettyArg i) :| [prettyArg es]
     Case _ arg cs -> iterAppDocM $ \_ prettyArg -> "case" :| [prettyArg arg, prettyArg (toList cs)]
+    Let _ ns t -> iterAppDocM $ \_ prettyArg ->
+      "let" :| [parens' (sep $ prettyArg <$> ns), prettyArg t]
+    Bind _ t bs -> iterAppDocM $ \_ prettyArg ->
+      "bind" :| [prettyArg t, prettyArg bs]
 
 instance
   (PrettyReadableBy configName (Term name uni fun a)) =>
diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Instance/Scoping.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Instance/Scoping.hs
index 043279c2662..198142897f7 100644
--- a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Instance/Scoping.hs
+++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Instance/Scoping.hs
@@ -50,6 +50,10 @@ instance name ~ Name => EstablishScoping (Term name uni fun) where
         -- that none of the transformations leak variables outside of the branch they're bound in.
         pure . referenceOutOfScope branchBounds $
             Case NotAName aScoped . Vector.fromList $ map referenceInBranch esScopedPoked
+    establishScoping (Let _ _ns _t) = error "no"
+    establishScoping (Bind _ _t _bs) = error "no"
+    -- TODO: Current scope checking uses `NameAnn` which only allows a single name to be annotated.
+    -- It's hard to support `Let` and `Bind` which binds multiple names at once
 
 instance name ~ Name => EstablishScoping (Program name uni fun) where
     establishScoping (Program _ ver term) = Program NotAName ver <$> establishScoping term
@@ -65,6 +69,8 @@ instance name ~ Name => CollectScopeInfo (Term name uni fun) where
     collectScopeInfo (Builtin _ _)          = mempty
     collectScopeInfo (Constr _ _ es)        = foldMap collectScopeInfo es
     collectScopeInfo (Case _ arg cs)        = collectScopeInfo arg <> foldMap collectScopeInfo cs
+    collectScopeInfo (Let _ _ns _t)         = error "no"
+    collectScopeInfo (Bind _ _t _bs)        = error "no"
 
 instance name ~ Name => CollectScopeInfo (Program name uni fun) where
     collectScopeInfo (Program _ _ term) = collectScopeInfo term
diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Plated.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Plated.hs
index bb2683bbd16..1da9ee4e634 100644
--- a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Plated.hs
+++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Plated.hs
@@ -32,6 +32,8 @@ termConstants f term0 = case term0 of
     Builtin{}        -> pure term0
     Constr{}         -> pure term0
     Case{}           -> pure term0
+    Let{}            -> pure term0
+    Bind{}           -> pure term0
 
 -- | Get all the direct child 'name a's of the given 'Term' from 'LamAbs'es.
 termBinds :: Traversal' (Term name uni fun ann) name
@@ -55,16 +57,18 @@ termUniques f = \case
 -- | Get all the direct child 'Term's of the given 'Term'.
 termSubterms :: Traversal' (Term name uni fun ann) (Term name uni fun ann)
 termSubterms f = \case
-    LamAbs ann n t    -> LamAbs ann n <$> f t
-    Apply ann t1 t2   -> Apply ann <$> f t1 <*> f t2
-    Delay ann t       -> Delay ann <$> f t
-    Force ann t       -> Force ann <$> f t
-    Constr ann i args -> Constr ann i <$> traverse f args
-    Case ann arg cs   -> Case ann <$> f arg <*> traverse f cs
-    e@Error {}        -> pure e
-    v@Var {}          -> pure v
-    c@Constant {}     -> pure c
-    b@Builtin {}      -> pure b
+    LamAbs ann n t     -> LamAbs ann n <$> f t
+    Apply ann t1 t2    -> Apply ann <$> f t1 <*> f t2
+    Delay ann t        -> Delay ann <$> f t
+    Force ann t        -> Force ann <$> f t
+    Constr ann i args  -> Constr ann i <$> traverse f args
+    Case ann arg cs    -> Case ann <$> f arg <*> traverse f cs
+    Let ann names body -> Let ann names <$> f body
+    Bind ann t binds   -> Bind ann <$> f t <*> traverse f binds
+    e@Error {}         -> pure e
+    v@Var {}           -> pure v
+    c@Constant {}      -> pure c
+    b@Builtin {}       -> pure b
 {-# INLINE termSubterms #-}
 
 -- | Get all the transitive child 'Constant's of the given 'Term'.
diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Type.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Type.hs
index 55e4d89d512..26d9b910cfc 100644
--- a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Type.hs
+++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Type.hs
@@ -101,6 +101,8 @@ data Term name uni fun ann
     | Constr !ann !Word64 ![Term name uni fun ann]
     -- See Note [Supported case-expressions].
     | Case !ann !(Term name uni fun ann) !(Vector (Term name uni fun ann))
+    | Let !ann ![name] !(Term name uni fun ann)
+    | Bind !ann !(Term name uni fun ann) ![Term name uni fun ann]
     deriving stock (Functor, Generic)
 
 deriving stock instance (Show name, GShow uni, Everywhere uni Show, Show fun, Show ann, Closed uni)
@@ -168,6 +170,8 @@ termAnn (Force ann _)    = ann
 termAnn (Error ann)      = ann
 termAnn (Constr ann _ _) = ann
 termAnn (Case ann _ _)   = ann
+termAnn (Let ann _ _)    = ann
+termAnn (Bind ann _ _)   = ann
 
 bindFunM
     :: Monad m
@@ -185,6 +189,8 @@ bindFunM f = go where
     go (Error ann)            = pure $ Error ann
     go (Constr ann i args)    = Constr ann i <$> traverse go args
     go (Case ann arg cs)      = Case ann <$> go arg <*> traverse go cs
+    go (Let ann name body)    = Let ann name <$> go body
+    go (Bind ann fun arg)     = Bind ann <$> go fun <*> traverse go arg
 
 bindFun
     :: (ann -> fun -> Term name uni fun' ann)
diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/DeBruijn.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/DeBruijn.hs
index f5d7960e413..7983f426943 100644
--- a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/DeBruijn.hs
+++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/DeBruijn.hs
@@ -93,6 +93,15 @@ deBruijnTermWithM h = go
        Constant ann con -> pure $ Constant ann con
        Builtin ann bn -> pure $ Builtin ann bn
        Error ann -> pure $ Error ann
+       Let ann names body -> do
+         let
+           goNames acc [] = Let ann (acc []) <$> go body
+           goNames acc (n:ns) = declareUnique n $ do
+             n' <- nameToDeBruijn h n
+             withScope $ do
+               goNames (acc . (n':)) ns
+         goNames id names
+       Bind ann t binds -> Bind ann <$> go t <*> traverse go binds
 
 -- | Takes a "handler" function to execute when encountering free variables.
 unDeBruijnTermWithM
@@ -121,3 +130,12 @@ unDeBruijnTermWithM h = go
         Constant ann con -> pure $ Constant ann con
         Builtin ann bn -> pure $ Builtin ann bn
         Error ann -> pure $ Error ann
+        Let ann names body -> do
+          let
+            goNames acc [] = Let ann (acc []) <$> go body
+            goNames acc (n:ns) = declareBinder $ do
+              n' <- deBruijnToName h $ set index deBruijnInitIndex n
+              withScope $ do
+                goNames (acc . (n':)) ns
+          goNames id names
+        Bind ann t binds -> Bind ann <$> go t <*> traverse go binds
diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs
index 8ad705e0ae8..6d64e1fc8a0 100644
--- a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs
+++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs
@@ -308,6 +308,7 @@ data CekValue uni fun ann =
       -- Check the docs of 'BuiltinRuntime' for details.
     -- | A constructor value, including fully computed arguments and the tag.
   | VConstr {-# UNPACK #-} !Word64 !(EmptyOrMultiStack uni fun ann)
+  | VLet ![NamedDeBruijn] !(NTerm uni fun ann) !(CekValEnv uni fun ann)
 
 deriving stock instance (GShow uni, Everywhere uni Show, Show fun, Show ann, Closed uni)
     => Show (CekValue uni fun ann)
@@ -458,6 +459,7 @@ they don't actually take the context as an argument even at the source level.
 -- | Implicit parameter for the builtin runtime.
 type GivenCekRuntime uni fun ann = (?cekRuntime :: BuiltinsRuntime fun (CekValue uni fun ann))
 type GivenCekCaserBuiltin uni = (?cekCaserBuiltin :: CaserBuiltin uni)
+type GivenCekLeterBuiltin uni = (?cekLeterBuiltin :: LeterBuiltin uni)
 -- | Implicit parameter for the log emitter reference.
 type GivenCekEmitter uni fun s = (?cekEmitter :: CekEmitter uni fun s)
 -- | Implicit parameter for budget spender.
@@ -470,6 +472,7 @@ type GivenCekCosts = (?cekCosts :: CekMachineCosts)
 type GivenCekReqs uni fun ann s =
     ( GivenCekRuntime uni fun ann
     , GivenCekCaserBuiltin uni
+    , GivenCekLeterBuiltin uni
     , GivenCekEmitter uni fun s
     , GivenCekSpender uni fun s
     , GivenCekSlippage
@@ -639,6 +642,11 @@ dischargeCekValue value0     = DischargeNonConstant $ goValue value0 where
         -- @term@ is fully discharged, so we can return it directly without any further discharging.
         VBuiltin _ term _ -> term
         VConstr ind args -> Constr () ind . map goValue $ argStackToList args
+        VLet names body env ->
+          Let
+            ()
+            ((\(NamedDeBruijn n _ix) -> NamedDeBruijn n deBruijnInitIndex) <$> names)
+            (goValEnv env 1 body)
 
     -- Instantiate all the free variables of a term by looking them up in an environment.
     -- Mutually recursive with @goValue@.
@@ -669,6 +677,8 @@ dischargeCekValue value0     = DischargeNonConstant $ goValue value0 where
           Error _            -> Error ()
           Constr _ ind args  -> Constr () ind $ map (go shift) args
           Case _ scrut alts  -> Case () (go shift scrut) $ fmap (go shift) alts
+          Let _ names body   -> Let () names (go (shift + fromIntegral (length names)) body)
+          Bind _ t bs        -> Bind () (go shift t) (fmap (go shift) bs)
 
 instance (PrettyUni uni, Pretty fun) => PrettyBy PrettyConfigPlc (CekValue uni fun ann) where
     prettyBy cfg = prettyBy cfg . dischargeResultToTerm . dischargeCekValue
@@ -705,6 +715,8 @@ data Context uni fun ann
     -- ^ @(constr i V0 ... Vj-1 _ Nj ... Nn)@
     | FrameCases !(CekValEnv uni fun ann) !(V.Vector (NTerm uni fun ann)) !(Context uni fun ann)
     -- ^ @(case _ C0 .. Cn)@
+    | FrameAwaitLetBinds !(CekValEnv uni fun ann) {-# UNPACK #-} !Word64 !(NTerm uni fun ann) ![NTerm uni fun ann] !(ArgStack uni fun ann) !(Context uni fun ann)
+    | FrameAwaitLet {-# UNPACK #-} !Word64 !(ArgStack uni fun ann) !(Context uni fun ann)
     | NoFrame
 
 deriving stock instance (GShow uni, Everywhere uni Show, Show fun, Show ann, Closed uni)
@@ -718,6 +730,7 @@ instance (Closed uni, uni `Everywhere` ExMemoryUsage) => ExMemoryUsage (CekValue
         VLamAbs {}  -> singletonRose 1
         VBuiltin {} -> singletonRose 1
         VConstr {}  -> singletonRose 1
+        VLet {}  -> singletonRose 1
     {-# INLINE memoryUsage #-}
 
 {- Note [ArgStack vs Spine]
@@ -743,7 +756,7 @@ runCekM
     -> (forall s. GivenCekReqs uni fun ann s => CekM uni fun s (DischargeResult uni fun))
     -> CekReport cost NamedDeBruijn uni fun
 runCekM
-        (MachineParameters caser (MachineVariantParameters costs runtime))
+        (MachineParameters caser leter (MachineVariantParameters costs runtime))
         (ExBudgetMode getExBudgetInfo)
         (EmitterMode getEmitterMode)
         a = runST $ do
@@ -752,6 +765,7 @@ runCekM
     ctr <- newCounter (Proxy @CounterSize)
     let ?cekRuntime = runtime
         ?cekCaserBuiltin = caser
+        ?cekLeterBuiltin = leter
         ?cekEmitter = _cekEmitterInfoEmit
         ?cekBudgetSpender = _exBudgetModeSpender
         ?cekCosts = costs
@@ -832,6 +846,16 @@ enterComputeCek = computeCek
     -- s ; ρ ▻ error  ↦  <> A
     computeCek !_ !_ (Error _) =
         throwErrorWithCause (OperationalError CekEvaluationFailure) (Error ())
+    -- ???
+    computeCek !ctx !env (Let _ names body) = do
+        stepAndMaybeSpend BLamAbs
+        returnCek ctx (VLet names body env)
+    computeCek !ctx !env (Bind _ body bs) = do
+        --stepAndMaybeSpend BApply
+        -- computeCek (FrameAwaitLetBinds env t bs ctx) env t
+        case bs of
+          (t : rest) -> computeCek (FrameAwaitLetBinds env 0 body rest NilStack ctx) env t
+          []         -> computeCek ctx env body
 
     {- | The returning phase of the CEK machine.
     Returns 'EvaluationSuccess' in case the context is empty, otherwise pops up one frame
@@ -871,6 +895,17 @@ enterComputeCek = computeCek
         SpineLast arg      -> applyEvaluate ctx fun (VCon arg)
         SpineCons arg rest -> applyEvaluate (FrameAwaitFunConN rest ctx) fun (VCon arg)
     -- s , [_ V1 .. Vn] ◅ lam x (M,ρ)  ↦  s , [_ V2 .. Vn]; ρ [ x  ↦  V1 ] ▻ M
+    returnCek (FrameAwaitLet cnt args ctx) l =
+      let
+        -- this can probably be done in FrameAwaitLetBinds for better performance.
+        go acc NilStack         = acc
+        go acc (ConsStack x xs) = Env.cons x (go acc xs)
+      in case l of
+           VLet names body env
+             | length names == fromIntegral cnt -> computeCek ctx (go env args) body
+             | otherwise -> error $ show (length names) <> " " <> show cnt
+           _               -> error "no"
+
     returnCek (FrameAwaitFunValueN args ctx) fun =
         case args of
           LastStackNonEmpty arg ->
@@ -903,8 +938,20 @@ enterComputeCek = computeCek
         VCon val -> case unCaserBuiltin ?cekCaserBuiltin val cs of
             Left err          -> throwErrorDischarged (OperationalError $ CekCaseBuiltinError err) e
             Right (HeadOnly fX) -> computeCek ctx env fX
-            Right (HeadSpine f xs) -> computeCek (FrameAwaitFunConN xs ctx) env f
+            Right (HeadSpine f xs) ->
+              let
+                -- we reverse and reverse again, this is bad, just POC
+                go acc (SpineLast x)      = (ConsStack (VCon x) acc, 1)
+                go acc (SpineCons x rest) = (+1) <$> go (ConsStack (VCon x) acc) rest
+
+                (xs', cnt) = go NilStack xs
+              in computeCek (FrameAwaitLet cnt xs' ctx) env f
         _ -> throwErrorDischarged (StructuralError NonConstrScrutinizedMachineError) e
+    returnCek (FrameAwaitLetBinds env cnt l todo done ctx) e =
+      case todo of
+        (next : todo') ->
+          computeCek (FrameAwaitLetBinds env (cnt + 1) l todo' (ConsStack e done) ctx) env next
+        []             -> computeCek (FrameAwaitLet (cnt + 1) (ConsStack e done) ctx) env l
 
     -- | @force@ a term and proceed.
     -- If v is a delay then compute the body of v;
@@ -961,6 +1008,15 @@ enterComputeCek = computeCek
                 evalBuiltinApp ctx fun term' $ f arg
             _ ->
                 throwErrorWithCause (StructuralError UnexpectedBuiltinTermArgumentMachineError) term'
+    applyEvaluate !ctx (VLet names body env) (VCon v) =
+      case unLeterBuiltin ?cekLeterBuiltin v of
+        Right binds
+          | length binds == length names ->
+            computeCek ctx (foldl (flip (Env.cons . VCon)) env binds) body
+          | otherwise -> error "aa"
+        Left e -> error $ show e
+
+      -- computeCek (FrameAwaitLet cnt xs' ctx) env body
     applyEvaluate !_ val _ =
         throwErrorDischarged (StructuralError NonFunctionalApplicationMachineError) val
 
diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/SteppableCek/Internal.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/SteppableCek/Internal.hs
index 9b1abd32a85..28747152ebd 100644
--- a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/SteppableCek/Internal.hs
+++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/SteppableCek/Internal.hs
@@ -347,7 +347,7 @@ mkCekTrans
     -> Slippage
     -> m (CekTrans uni fun ann s, ExBudgetInfo cost uni fun s)
 mkCekTrans
-        (MachineParameters caser (MachineVariantParameters costs runtime))
+        (MachineParameters caser leter (MachineVariantParameters costs runtime))
         (ExBudgetMode getExBudgetInfo)
         (EmitterMode getEmitterMode)
         slippage = do
@@ -356,6 +356,7 @@ mkCekTrans
     ctr <- newCounter (Proxy @CounterSize)
     let ?cekRuntime = runtime
         ?cekCaserBuiltin = caser
+        ?cekLeterBuiltin = leter
         ?cekEmitter = _cekEmitterInfoEmit
         ?cekBudgetSpender = _exBudgetModeSpender
         ?cekCosts = costs
diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Parser.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Parser.hs
index 1e1de0484be..0c521e54aa7 100644
--- a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Parser.hs
+++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Parser.hs
@@ -90,6 +90,20 @@ caseTerm = withSpan $ \sp ->
       whenVersion (\v -> v < plcVersion110) $ fail "'case' is not allowed before version 1.1.0"
       pure res
 
+letTerm :: Parser PTerm
+letTerm = withSpan $ \sp ->
+  inParens $ symbol "let" *> do
+    res <- UPLC.Let sp <$> (inParens $ many (leadingWhitespace name)) <*> term
+    -- TODO: version check
+    pure res
+
+bindTerm :: Parser PTerm
+bindTerm = withSpan $ \sp ->
+  inParens $ symbol "bind" *> do
+    res <- UPLC.Bind sp <$> term <*> (many term)
+    -- TODO: version check
+    pure res
+
 -- | Parser for all UPLC terms.
 term :: Parser PTerm
 term = leadingWhitespace go
@@ -106,6 +120,8 @@ term = leadingWhitespace go
             , errorTerm
             , constrTerm
             , caseTerm
+            , letTerm
+            , bindTerm
             ]
 
 -- | Parser for UPLC programs.
diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Rename/Internal.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Rename/Internal.hs
index 3389dda5e69..cbd0dcbf888 100644
--- a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Rename/Internal.hs
+++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Rename/Internal.hs
@@ -35,6 +35,12 @@ renameTermM (Constr ann i es)          = Constr ann i <$> traverse renameTermM e
 renameTermM (Case ann arg cs)          = Case ann <$> renameTermM arg <*> traverse renameTermM cs
 renameTermM con@Constant{}             = pure con
 renameTermM bi@Builtin{}               = pure bi
+renameTermM (Let ann names body)       =
+  let
+    goNames acc []     = Let ann (acc []) <$> renameTermM body
+    goNames acc (n:ns) = withFreshenedName n $ \n' -> goNames (acc . (n':)) ns
+  in goNames id names
+renameTermM (Bind ann t binds) = Bind ann <$> renameTermM t <*> traverse renameTermM binds
 
 -- | Rename a 'Program' in the 'RenameM' monad.
 renameProgramM
diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Subst.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Subst.hs
index e6495a113ad..564f7fcc536 100644
--- a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Subst.hs
+++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Subst.hs
@@ -72,6 +72,8 @@ termMapNames f = go
             Force ann t          -> Force ann (go t)
             Constr ann i es      -> Constr ann i (fmap go es)
             Case ann arg cs      -> Case ann (go arg) (fmap go cs)
+            Let ann ns t         -> Let ann (fmap f ns) (go t)
+            Bind ann t bs        -> Bind ann (go t) (fmap go bs)
 
             Constant ann c       -> Constant ann c
             Builtin ann b        -> Builtin ann b