diff --git a/Cslib.lean b/Cslib.lean
index 63f454f4..611bcb59 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -26,9 +26,11 @@ public import Cslib.Computability.Languages.Language
 public import Cslib.Computability.Languages.OmegaLanguage
 public import Cslib.Computability.Languages.OmegaRegularLanguage
 public import Cslib.Computability.Languages.RegularLanguage
+public import Cslib.Computability.Machines.SingleTapeTuring.Basic
 public import Cslib.Foundations.Control.Monad.Free
 public import Cslib.Foundations.Control.Monad.Free.Effects
 public import Cslib.Foundations.Control.Monad.Free.Fold
+public import Cslib.Foundations.Data.BiTape
 public import Cslib.Foundations.Data.FinFun
 public import Cslib.Foundations.Data.HasFresh
 public import Cslib.Foundations.Data.Nat.Segment
@@ -40,6 +42,7 @@ public import Cslib.Foundations.Data.OmegaSequence.Temporal
 public import Cslib.Foundations.Data.RelatesInSteps
 public import Cslib.Foundations.Data.Relation
 public import Cslib.Foundations.Data.Set.Saturation
+public import Cslib.Foundations.Data.StackTape
 public import Cslib.Foundations.Lint.Basic
 public import Cslib.Foundations.Semantics.FLTS.Basic
 public import Cslib.Foundations.Semantics.FLTS.FLTSToLTS
diff --git a/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean b/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean
new file mode 100644
index 00000000..dee64200
--- /dev/null
+++ b/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean
@@ -0,0 +1,490 @@
+/-
+Copyright (c) 2026 Bolton Bailey. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bolton Bailey, Pim Spelier, Daan van Gent
+-/
+
+module
+
+public import Cslib.Foundations.Data.BiTape
+public import Cslib.Foundations.Data.RelatesInSteps
+public import Mathlib.Algebra.Polynomial.Eval.Defs
+
+@[expose] public section
+
+/-!
+# Single-Tape Turing Machines
+
+Defines a single-tape Turing machine for computing functions on `List α` for finite alphabet `α`.
+These machines have access to a single bidirectionally-infinite tape (`BiTape`)
+which uses symbols from `Option α`.
+
+## Important Declarations
+
+We define a number of structures related to Turing machine computation:
+
+* `Stmt`: the write and movement operations a TM can do in a single step.
+* `SingleTapeTM`: the TM itself.
+* `Cfg`: the configuration of a TM, including internal and tape state.
+* `TimeComputable f`: a TM for computing `f`, packaged with a bound on runtime.
+* `PolyTimeComputable f`: `TimeComputable f` packaged with a polynomial bound on runtime.
+
+We also provide ways of constructing polynomial-runtime TMs
+
+* `PolyTimeComputable.id`: computes the identity function
+* `PolyTimeComputable.comp`: computes the composition of polynomial time machines
+
+## TODOs
+
+- Encoding of types in lists to represent computations on arbitrary types.
+- Add `∘` notation for `compComputer`.
+
+-/
+
+open Cslib Relation
+
+namespace Turing
+
+open BiTape StackTape
+
+variable {α : Type}
+
+namespace SingleTapeTM
+
+/--
+A Turing machine "statement" is just a `Option`al command to move left or right,
+and write a symbol (i.e. an `Option α`, where `none` is the blank symbol) on the `BiTape`
+-/
+structure Stmt (α : Type) where
+  /-- The symbol to write at the current head position -/
+  symbol : Option α
+  /-- The direction to move the tape head -/
+  movement : Option Dir
+deriving Inhabited
+
+end SingleTapeTM
+
+/--
+A single-tape Turing machine
+over the alphabet of `Option α` (where `none` is the blank `BiTape` symbol).
+-/
+structure SingleTapeTM α where
+  /-- Inhabited instance for the alphabet -/
+  [αInhabited : Inhabited α]
+  /-- Finiteness of the alphabet -/
+  [αFintype : Fintype α]
+  /-- type of state labels -/
+  (Λ : Type)
+  /-- finiteness of the state type -/
+  [ΛFintype : Fintype Λ]
+  /-- Initial state -/
+  (q₀ : Λ)
+  /-- Transition function, mapping a state and a head symbol to a `Stmt` to invoke,
+  and optionally the new state to transition to afterwards (`none` for halt) -/
+  (M : Λ → Option α → SingleTapeTM.Stmt α × Option Λ)
+
+namespace SingleTapeTM
+
+section Cfg
+
+/-!
+## Configurations of a Turing Machine
+
+This section defines the configurations of a Turing machine,
+the step function that lets the machine transition from one configuration to the next,
+and the intended initial and final configurations.
+-/
+
+variable (tm : SingleTapeTM α)
+
+instance : Inhabited tm.Λ := ⟨tm.q₀⟩
+
+instance : Fintype tm.Λ := tm.ΛFintype
+
+instance inhabitedStmt : Inhabited (Stmt α) := inferInstance
+
+/--
+The configurations of a Turing machine consist of:
+an `Option`al state (or none for the halting state),
+and a `BiTape` representing the tape contents.
+-/
+structure Cfg : Type where
+  /-- the state of the TM (or none for the halting state) -/
+  state : Option tm.Λ
+  /-- the BiTape contents -/
+  BiTape : BiTape α
+deriving Inhabited
+
+/-- The step function corresponding to a `SingleTapeTM`. -/
+@[simp]
+def step : tm.Cfg → Option tm.Cfg
+  | ⟨none, _⟩ =>
+    -- If in the halting state, there is no next configuration
+    none
+  | ⟨some q', t⟩ =>
+    -- If in state q', perform look up in the transition function
+    match tm.M q' t.head with
+    -- and enter a new configuration with state q'' (or none for halting)
+    -- and tape updated according to the Stmt
+    | ⟨⟨wr, dir⟩, q''⟩ => some ⟨q'', (t.write wr).optionMove dir⟩
+
+/--
+The initial configuration corresponding to a list in the input alphabet.
+Note that the entries of the tape constructed by `BiTape.mk₁` are all `some` values.
+This is to ensure that distinct lists map to distinct initial configurations.
+-/
+def initCfg (tm : SingleTapeTM α) (s : List α) : tm.Cfg := ⟨some tm.q₀, BiTape.mk₁ s⟩
+
+/-- The final configuration corresponding to a list in the output alphabet.
+(We demand that the head halts at the leftmost position of the output.)
+-/
+def haltCfg (tm : SingleTapeTM α) (s : List α) : tm.Cfg := ⟨none, BiTape.mk₁ s⟩
+
+/--
+The space used by a configuration is the space used by its tape.
+-/
+def Cfg.space_used (tm : SingleTapeTM α) (cfg : tm.Cfg) : ℕ := cfg.BiTape.space_used
+
+@[scoped grind =]
+lemma Cfg.space_used_initCfg (tm : SingleTapeTM α) (s : List α) :
+    (tm.initCfg s).space_used = max 1 s.length := BiTape.space_used_mk₁ s
+
+@[scoped grind =]
+lemma Cfg.space_used_haltCfg (tm : SingleTapeTM α) (s : List α) :
+    (tm.haltCfg s).space_used = max 1 s.length := BiTape.space_used_mk₁ s
+
+lemma Cfg.space_used_step {tm : SingleTapeTM α} (cfg cfg' : tm.Cfg)
+    (hstep : tm.step cfg = some cfg') : cfg'.space_used ≤ cfg.space_used + 1 := by
+  obtain ⟨_ | q, tape⟩ := cfg
+  · simp [step] at hstep
+  · simp only [step] at hstep
+    generalize hM : tm.M q tape.head = result at hstep
+    obtain ⟨⟨wr, dir⟩, q''⟩ := result
+    cases hstep; cases dir with
+    | none => simp [Cfg.space_used, BiTape.optionMove, BiTape.space_used_write, hM]
+    | some d => simpa [Cfg.space_used, BiTape.optionMove, BiTape.space_used_write, hM] using
+        BiTape.space_used_move (tape.write wr) d
+
+end Cfg
+
+open Cfg
+
+/--
+The `TransitionRelation` corresponding to a `SingleTapeTM α`
+is defined by the `step` function,
+which maps a configuration to its next configuration, if it exists.
+-/
+@[scoped grind =]
+def TransitionRelation (tm : SingleTapeTM α) (c₁ c₂ : tm.Cfg) : Prop := tm.step c₁ = some c₂
+
+/-- A proof of `tm` outputting `l'` on input `l`. -/
+def Outputs (tm : SingleTapeTM α) (l l' : List α) : Prop :=
+  ReflTransGen tm.TransitionRelation (initCfg tm l) (haltCfg tm l')
+
+/-- A proof of `tm` outputting `l'` on input `l` in at most `m` steps. -/
+def OutputsWithinTime (tm : SingleTapeTM α) (l l' : List α) (m : ℕ) :=
+  RelatesWithinSteps tm.TransitionRelation (initCfg tm l) (haltCfg tm l') m
+
+/--
+This lemma bounds the size blow-up of the output of a Turing machine.
+It states that the increase in length of the output over the input is bounded by the runtime.
+This is important for guaranteeing that composition of polynomial time Turing machines
+remains polynomial time, as the input to the second machine
+is bounded by the output length of the first machine.
+-/
+lemma output_length_le_input_length_add_time (tm : SingleTapeTM α) (l l' : List α) (t : ℕ)
+    (h : tm.OutputsWithinTime l l' t) :
+    l'.length ≤ max 1 l.length + t := by
+  obtain ⟨steps, hsteps_le, hevals⟩ := h
+  grind [hevals.apply_le_apply_add (Cfg.space_used tm)
+      fun a b hstep ↦ Cfg.space_used_step a b (Option.mem_def.mp hstep)]
+
+section Computers
+
+variable [Inhabited α] [Fintype α]
+
+/-- A Turing machine computing the identity. -/
+def idComputer : SingleTapeTM α where
+  Λ := PUnit
+  q₀ := PUnit.unit
+  M _ b := ⟨⟨b, none⟩, none⟩
+
+/--
+A Turing machine computing the composition of two other Turing machines.
+
+If f and g are computed by Turing machines `tm1` and `tm2`
+then we can construct a Turing machine which computes g ∘ f by first running `tm1`
+and then, when `tm1` halts, transitioning to the start state of `tm2` and running `tm2`.
+-/
+def compComputer (tm1 tm2 : SingleTapeTM α) : SingleTapeTM α where
+  -- The states of the composed machine are the disjoint union of the states of the input machines.
+  Λ := tm1.Λ ⊕ tm2.Λ
+  -- The start state is the start state of the first input machine.
+  q₀ := .inl tm1.q₀
+  M q h :=
+    match q with
+    -- If we are in the first input machine's states, run that machine ...
+    | .inl ql => match tm1.M ql h with
+      | (stmt, state) =>
+        -- ... taking the same tape action as the first input machine would.
+        (stmt,
+          match state with
+          -- If it halts, transition to the start state of the second input machine
+          | none => some (.inr tm2.q₀)
+          -- Otherwise continue as normal
+          | _ => Option.map .inl state)
+    -- If we are in the second input machine's states, run that machine ...
+    | .inr qr =>
+      match tm2.M qr h with
+      | (stmt, state) =>
+        -- ... taking the same tape action as the second input machine would.
+        (stmt,
+          match state with
+          -- If it halts, transition to the halting state
+          | none => none
+          -- Otherwise continue as normal
+          | _ => Option.map .inr state)
+
+section compComputerLemmas
+
+/-! ### Composition Computer Lemmas -/
+
+variable (tm1 tm2 : SingleTapeTM α) (cfg1 : tm1.Cfg) (cfg2 : tm2.Cfg)
+
+lemma compComputer_q₀_eq : (compComputer tm1 tm2).q₀ = Sum.inl tm1.q₀ := rfl
+
+/--
+Convert a `Cfg` over the first input machine to a config over the composed machine.
+Note it may transition to the start state of the second machine if the first machine halts.
+-/
+private def toCompCfg_left : (compComputer tm1 tm2).Cfg :=
+  match cfg1.state with
+  | some q => ⟨some (Sum.inl q), cfg1.BiTape⟩
+  | none => ⟨some (Sum.inr tm2.q₀), cfg1.BiTape⟩
+
+/-- Convert a `Cfg` over the second input machine to a config over the composed machine -/
+private def toCompCfg_right : (compComputer tm1 tm2).Cfg :=
+  ⟨Option.map Sum.inr cfg2.state, cfg2.BiTape⟩
+
+/-- The initial configuration for the composed machine, with the first machine starting. -/
+private def initialCfg (input : List α) : (compComputer tm1 tm2).Cfg :=
+  ⟨some (Sum.inl tm1.q₀), BiTape.mk₁ input⟩
+
+/-- The intermediate configuration for the composed machine,
+after the first machine halts and the second machine starts. -/
+private def intermediateCfg (intermediate : List α) : (compComputer tm1 tm2).Cfg :=
+  ⟨some (Sum.inr tm2.q₀), BiTape.mk₁ intermediate⟩
+
+/-- The final configuration for the composed machine, after the second machine halts. -/
+private def finalCfg (output : List α) : (compComputer tm1 tm2).Cfg :=
+  ⟨none, BiTape.mk₁ output⟩
+
+/-- The left converting function commutes with steps of the machines. -/
+private theorem map_toCompCfg_left_step (hcfg1 : cfg1.state.isSome) :
+    Option.map (toCompCfg_left tm1 tm2) (tm1.step cfg1) =
+      (compComputer tm1 tm2).step (toCompCfg_left tm1 tm2 cfg1) := by
+  cases cfg1 with | mk state BiTape => cases state with
+    | none => grind
+    | some q =>
+      simp only [step, toCompCfg_left, compComputer]
+      generalize hM : tm1.M q BiTape.head = result
+      obtain ⟨⟨wr, dir⟩, nextState⟩ := result
+      cases nextState <;> grind [toCompCfg_left]
+
+/-- The right converting function commutes with steps of the machines. -/
+private theorem map_toCompCfg_right_step :
+    Option.map (toCompCfg_right tm1 tm2) (tm2.step cfg2) =
+      (compComputer tm1 tm2).step (toCompCfg_right tm1 tm2 cfg2) := by
+  cases cfg2 with
+  | mk state BiTape =>
+    cases state with
+    | none =>
+      simp only [step, toCompCfg_right, Option.map_none, compComputer]
+    | some q =>
+      generalize hM : tm2.M q BiTape.head = result
+      obtain ⟨⟨wr, dir⟩, nextState⟩ := result
+      simp only [compComputer]
+      grind [toCompCfg_right, step, compComputer]
+
+/--
+Simulation for the first phase of the composed computer.
+When the first machine runs from start to halt, the composed machine
+runs from start (with Sum.inl state) to Sum.inr tm2.q₀ (the start of the second phase).
+This takes the same number of steps because the halt transition becomes a transition to the
+second machine.
+-/
+private theorem comp_left_relatesWithinSteps (input intermediate : List α) (t : ℕ)
+    (htm1 :
+      RelatesWithinSteps tm1.TransitionRelation
+        (tm1.initCfg input)
+        (tm1.haltCfg intermediate)
+        t) :
+    RelatesWithinSteps (compComputer tm1 tm2).TransitionRelation
+      (initialCfg tm1 tm2 input)
+      (intermediateCfg tm1 tm2 intermediate)
+      t := by
+  simp only [initialCfg, intermediateCfg, initCfg, haltCfg] at htm1 ⊢
+  refine RelatesWithinSteps.map (toCompCfg_left tm1 tm2) ?_ htm1
+  intro a b hab
+  have ha : a.state.isSome := by
+    simp only [TransitionRelation, step] at hab
+    cases a with | mk state _ => cases state <;> simp_all
+  have h1 := map_toCompCfg_left_step tm1 tm2 a ha
+  rw [hab, Option.map_some] at h1
+  exact h1.symm
+
+/--
+Simulation for the second phase of the composed computer.
+When the second machine runs from start to halt, the composed machine
+runs from Sum.inr tm2.q₀ to halt.
+-/
+private theorem comp_right_relatesWithinSteps (intermediate output : List α) (t : ℕ)
+    (htm2 :
+      RelatesWithinSteps tm2.TransitionRelation
+        (tm2.initCfg intermediate)
+        (tm2.haltCfg output)
+        t) :
+    RelatesWithinSteps (compComputer tm1 tm2).TransitionRelation
+      (intermediateCfg tm1 tm2 intermediate)
+      (finalCfg tm1 tm2 output)
+      t := by
+  simp only [intermediateCfg, finalCfg, initCfg, haltCfg] at htm2 ⊢
+  refine RelatesWithinSteps.map (toCompCfg_right tm1 tm2) ?_ htm2
+  intro a b hab
+  grind [map_toCompCfg_right_step tm1 tm2 a]
+
+end compComputerLemmas
+
+end Computers
+
+/-!
+## Time Computability
+
+This section defines the notion of time-bounded Turing Machines
+-/
+
+section TimeComputable
+
+variable [Inhabited α] [Fintype α]
+
+/-- A Turing machine + a time function +
+a proof it outputs `f` in at most `time(input.length)` steps. -/
+structure TimeComputable (f : List α → List α) where
+  /-- the underlying bundled SingleTapeTM -/
+  tm : SingleTapeTM α
+  /-- a bound on runtime -/
+  time_bound : ℕ → ℕ
+  /-- proof this machine outputs `f` in at most `time_bound(input.length)` steps -/
+  outputsFunInTime (a) : tm.OutputsWithinTime a (f a) (time_bound a.length)
+
+
+/-- The identity map on α is computable in constant time. -/
+def TimeComputable.id : TimeComputable (α := α) id where
+  tm := idComputer
+  time_bound _ := 1
+  outputsFunInTime _ := ⟨1, le_rfl, RelatesInSteps.single rfl⟩
+
+/--
+Time bounds for `compComputer`.
+
+The `compComputer` of two machines which have time bounds is bounded by
+
+* The time taken by the first machine on the input size
+* added to the time taken by the second machine on the output size of the first machine
+  (which is itself bounded by the time taken by the first machine)
+
+Note that we require the time function of the second machine to be monotone;
+this is to ensure that if the first machine returns an output
+which is shorter than the maximum possible length of output for that input size,
+then the time bound for the second machine still holds for that shorter input to the second machine.
+-/
+def TimeComputable.comp {f g : List α → List α} (hf : TimeComputable f) (hg : TimeComputable g)
+    (h_mono : Monotone hg.time_bound) :
+    (TimeComputable (g ∘ f)) where
+  tm := compComputer hf.tm hg.tm
+  -- perhaps it would be good to track the blow up separately?
+  time_bound l := (hf.time_bound l) + hg.time_bound (max 1 l + hf.time_bound l)
+  outputsFunInTime a := by
+    have hf_outputsFun := hf.outputsFunInTime a
+    have hg_outputsFun := hg.outputsFunInTime (f a)
+    simp only [OutputsWithinTime, initCfg, compComputer_q₀_eq, Function.comp_apply,
+      haltCfg] at hg_outputsFun hf_outputsFun ⊢
+    -- The computer reduces a to f a in time hf.time_bound a.length
+    have h_a_reducesTo_f_a :
+        RelatesWithinSteps (compComputer hf.tm hg.tm).TransitionRelation
+          (initialCfg hf.tm hg.tm a)
+          (intermediateCfg hf.tm hg.tm (f a))
+          (hf.time_bound a.length) :=
+      comp_left_relatesWithinSteps hf.tm hg.tm a (f a)
+        (hf.time_bound a.length) hf_outputsFun
+    -- The computer reduces f a to g (f a) in time hg.time_bound (f a).length
+    have h_f_a_reducesTo_g_f_a :
+        RelatesWithinSteps (compComputer hf.tm hg.tm).TransitionRelation
+          (intermediateCfg hf.tm hg.tm (f a))
+          (finalCfg hf.tm hg.tm (g (f a)))
+          (hg.time_bound (f a).length) :=
+      comp_right_relatesWithinSteps hf.tm hg.tm (f a) (g (f a))
+        (hg.time_bound (f a).length) hg_outputsFun
+    -- Therefore, the computer reduces a to g (f a) in the sum of those times.
+    have h_a_reducesTo_g_f_a := RelatesWithinSteps.trans h_a_reducesTo_f_a h_f_a_reducesTo_g_f_a
+    apply RelatesWithinSteps.of_le h_a_reducesTo_g_f_a
+    refine Nat.add_le_add_left ?_ (hf.time_bound a.length)
+    · apply h_mono
+      -- Use the lemma about output length being bounded by input length + time
+      exact output_length_le_input_length_add_time hf.tm _ _ _ (hf.outputsFunInTime a)
+
+end TimeComputable
+
+/-!
+## Polynomial Time Computability
+
+This section defines polynomial time computable functions on Turing machines,
+and proves that:
+
+* The identity function is polynomial time computable
+* The composition of two polynomial time computable functions is polynomial time computable
+
+-/
+
+section PolyTimeComputable
+
+open Polynomial
+
+variable [Inhabited α] [Fintype α]
+
+/-- A Turing machine + a polynomial time function +
+a proof it outputs `f` in at most `time(input.length)` steps. -/
+structure PolyTimeComputable (f : List α → List α) extends TimeComputable f where
+  /-- a polynomial time bound -/
+  poly : Polynomial ℕ
+  /-- proof that this machine outputs `f` in at most `time(input.length)` steps -/
+  bounds : ∀ n, time_bound n ≤ poly.eval n
+
+/-- A proof that the identity map on α is computable in polytime. -/
+noncomputable def PolyTimeComputable.id : @PolyTimeComputable (α := α) id where
+  toTimeComputable := TimeComputable.id
+  poly := 1
+  bounds _ := by simp [TimeComputable.id]
+
+-- TODO remove `h_mono` assumption
+-- by developing function to convert PolyTimeComputable into one with monotone time bound
+/--
+A proof that the composition of two polytime computable functions is polytime computable.
+-/
+noncomputable def PolyTimeComputable.comp {f g : List α → List α}
+    (hf : PolyTimeComputable f) (hg : PolyTimeComputable g)
+    (h_mono : Monotone hg.time_bound) :
+    PolyTimeComputable (g ∘ f) where
+  toTimeComputable := TimeComputable.comp hf.toTimeComputable hg.toTimeComputable h_mono
+  poly := hf.poly + hg.poly.comp (1 + X + hf.poly)
+  bounds n := by
+    simp only [TimeComputable.comp, eval_add, eval_comp, eval_X, eval_one]
+    apply add_le_add
+    · exact hf.bounds n
+    · exact (h_mono (add_le_add (by omega) (hf.bounds n))).trans (hg.bounds _)
+
+end PolyTimeComputable
+
+end SingleTapeTM
+
+end Turing
diff --git a/Cslib/Foundations/Data/BiTape.lean b/Cslib/Foundations/Data/BiTape.lean
new file mode 100644
index 00000000..0daa7bbc
--- /dev/null
+++ b/Cslib/Foundations/Data/BiTape.lean
@@ -0,0 +1,143 @@
+/-
+Copyright (c) 2026 Bolton Bailey. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bolton Bailey
+-/
+
+module
+
+public import Cslib.Foundations.Data.StackTape
+public import Mathlib.Computability.TuringMachine
+
+@[expose] public section
+
+/-!
+# BiTape: Bidirectionally infinite TM tape representation using StackTape
+
+This file defines `BiTape`, a tape representation for Turing machines
+in the form of an `List` of `Option` values,
+with the additional property that the list cannot end with `none`.
+
+## Design
+
+Note that Mathlib has a `Tape` type, but it requires the alphabet type to be inhabited,
+and considers the ends of the tape to be filled with default values.
+
+This design requires the tape elements to be `Option` values, and ensures that
+`List`s of the base alphabet, rendered directly onto the tape by mapping over `some`,
+will not collide.
+
+## Main definitions
+
+* `BiTape`: A tape with a head symbol and left/right contents stored as `StackTape`
+* `BiTape.move`: Move the tape head left or right
+* `BiTape.write`: Write a symbol at the current head position
+* `BiTape.space_used`: The space used by the tape
+-/
+
+namespace Turing
+
+/--
+A structure for bidirectionally-infinite Turing machine tapes
+that eventually take on blank `none` values
+-/
+structure BiTape (α : Type) where
+  /-- The symbol currently under the tape head -/
+  head : Option α
+  /-- The contents to the left of the head -/
+  left : StackTape α
+  /-- The contents to the right of the head -/
+  right : StackTape α
+
+namespace BiTape
+
+/-- The empty `BiTape` -/
+def nil {α} : BiTape α := ⟨none, ∅, ∅⟩
+
+instance {α : Type} : Inhabited (BiTape α) where
+  default := nil
+
+instance {α : Type} : EmptyCollection (BiTape α) :=
+  ⟨nil⟩
+
+@[simp]
+lemma empty_eq_nil {α} : (∅ : BiTape α) = nil := rfl
+
+/--
+Given a `List` of `α`, construct a `BiTape` by mapping the list to `some` elements
+and laying them out to the right side,
+with the head under the first element of the list if it exists.
+-/
+def mk₁ {α} (l : List α) : BiTape α :=
+  match l with
+  | [] => ∅
+  | h :: t => { head := some h, left := ∅, right := StackTape.map_some t }
+
+section Move
+
+/--
+Move the head left by shifting the left StackTape under the head.
+-/
+def move_left {α} (t : BiTape α) : BiTape α :=
+  ⟨t.left.head, t.left.tail, StackTape.cons t.head t.right⟩
+
+/--
+Move the head right by shifting the right StackTape under the head.
+-/
+def move_right {α} (t : BiTape α) : BiTape α :=
+  ⟨t.right.head, StackTape.cons t.head t.left, t.right.tail⟩
+
+/--
+Move the head to the left or right, shifting the tape underneath it.
+-/
+def move {α} (t : BiTape α) : Dir → BiTape α
+  | .left => t.move_left
+  | .right => t.move_right
+
+/--
+Optionally perform a `move`, or do nothing if `none`.
+-/
+def optionMove {α} : BiTape α → Option Dir → BiTape α
+  | t, none => t
+  | t, some d => t.move d
+
+@[simp]
+lemma move_left_move_right {α} (t : BiTape α) : t.move_left.move_right = t := by
+  simp [move_right, move_left]
+
+@[simp]
+lemma move_right_move_left {α} (t : BiTape α) : t.move_right.move_left = t := by
+  simp [move_left, move_right]
+
+end Move
+
+/--
+Write a value under the head of the `BiTape`.
+-/
+def write {α} (t : BiTape α) (a : Option α) : BiTape α := { t with head := a }
+
+/--
+The space used by a `BiTape` is the number of symbols
+between and including the head, and leftmost and rightmost non-blank symbols on the `BiTape`.
+-/
+@[scoped grind]
+def space_used {α} (t : BiTape α) : ℕ := 1 + t.left.length + t.right.length
+
+@[simp, grind =]
+lemma space_used_write {α} (t : BiTape α) (a : Option α) :
+    (t.write a).space_used = t.space_used := by rfl
+
+lemma space_used_mk₁ {α} (l : List α) :
+    (mk₁ l).space_used = max 1 l.length := by
+  cases l with
+  | nil => simp [mk₁, space_used, nil, StackTape.length_nil]
+  | cons h t => simp [mk₁, space_used, StackTape.length_nil, StackTape.length_map_some]; omega
+
+lemma space_used_move {α} (t : BiTape α) (d : Dir) :
+    (t.move d).space_used ≤ t.space_used + 1 := by
+  cases d <;> grind [move_left, move_right, move,
+    space_used, StackTape.length_tail_le, StackTape.length_cons_le]
+
+end BiTape
+
+end Turing
diff --git a/Cslib/Foundations/Data/RelatesInSteps.lean b/Cslib/Foundations/Data/RelatesInSteps.lean
index 07c66d0f..04106f01 100644
--- a/Cslib/Foundations/Data/RelatesInSteps.lean
+++ b/Cslib/Foundations/Data/RelatesInSteps.lean
@@ -124,9 +124,8 @@ lemma RelatesInSteps.succ'_iff {a b : α} {n : ℕ} :
 If `h : α → ℕ` increases by at most 1 on each step of `r`,
 then the value of `h` at the output is at most `h` at the input plus the number of steps.
 -/
-lemma RelatesInSteps.apply_le_apply_add {a b : α} (h : α → ℕ)
-    (h_step : ∀ a b, r a b → h b ≤ h a + 1)
-    (m : ℕ) (hevals : RelatesInSteps r a b m) :
+lemma RelatesInSteps.apply_le_apply_add {a b : α} {m : ℕ} (hevals : RelatesInSteps r a b m)
+    (h : α → ℕ) (h_step : ∀ a b, r a b → h b ≤ h a + 1) :
     h b ≤ h a + m := by
   induction hevals with
   | refl => simp
@@ -200,12 +199,12 @@ lemma RelatesWithinSteps.of_le {a b : α} {n₁ n₂ : ℕ}
 
 /-- If `h : α → ℕ` increases by at most 1 on each step of `r`,
 then the value of `h` at the output is at most `h` at the input plus the step bound. -/
-lemma RelatesWithinSteps.apply_le_apply_add {a b : α} (h : α → ℕ)
-    (h_step : ∀ a b, r a b → h b ≤ h a + 1)
-    (n : ℕ) (hevals : RelatesWithinSteps r a b n) :
-    h b ≤ h a + n := by
+lemma RelatesWithinSteps.apply_le_apply_add {a b : α} {m : ℕ} (hevals : RelatesWithinSteps r a b m)
+    (h : α → ℕ) (h_step : ∀ a b, r a b → h b ≤ h a + 1)
+    :
+    h b ≤ h a + m := by
   obtain ⟨m, hm, hevals_m⟩ := hevals
-  have := RelatesInSteps.apply_le_apply_add h h_step m hevals_m
+  have := RelatesInSteps.apply_le_apply_add hevals_m h h_step
   lia
 
 /--
diff --git a/Cslib/Foundations/Data/StackTape.lean b/Cslib/Foundations/Data/StackTape.lean
new file mode 100644
index 00000000..08814a04
--- /dev/null
+++ b/Cslib/Foundations/Data/StackTape.lean
@@ -0,0 +1,177 @@
+/-
+Copyright (c) 2026 Bolton Bailey. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bolton Bailey
+-/
+
+module
+
+public import Cslib.Init
+public import Mathlib.Data.List.Basic
+
+@[expose] public section
+
+/-!
+# StackTape: Infinite, eventually-`none` lists of `Option`s
+
+This file defines `StackTape`, a stack-like data structure of `Option` values,
+where the tape is considered to be infinite and eventually all `none`s.
+This is useful as a data structure with a simple API for manipulation by Turing machines.
+
+## Design
+
+`StackTape` is represented as a list of `Option` values where the list cannot end with `none`.
+The end of the list is then treated as the start of an infinite sequence of `none` values
+by the low-level API.
+This design makes it convenient to express the length of the tape in terms of the list length.
+
+An alternative design would be to represent the tape as a `Stream' (Option α)`,
+with additional fields tracking the length and the fact that the stream eventually becomes `none`.
+This design might complicate reasoning about the length of the tape, but could make other operations
+more straightforward.
+
+Future design work might explore this alternative representation and compare its
+advantages and disadvantages.
+
+## TODO
+
+- Make a `::`-like notation.
+
+-/
+
+namespace Turing
+
+/--
+An infinite tape representation using a list of `Option` values,
+where the list is eventually `none`.
+
+Represented as a `List (Option α)` that does not end with `none`.
+-/
+structure StackTape (α : Type) where
+  /-- The underlying list representation -/
+  toList : List (Option α)
+  /--
+  The list can be empty (i.e. `none`),
+  but if it is not empty, the last element is not (`some`) `none`
+  -/
+  toList_getLast?_ne_some_none : toList.getLast? ≠ some none
+
+attribute [scoped grind! .] StackTape.toList_getLast?_ne_some_none
+
+namespace StackTape
+
+/-- The empty `StackTape` -/
+@[scoped grind]
+def nil {α} : StackTape α := ⟨[], by grind⟩
+
+instance {α : Type} : Inhabited (StackTape α) where
+  default := nil
+
+instance {α : Type} : EmptyCollection (StackTape α) :=
+  ⟨nil⟩
+
+@[simp]
+lemma empty_eq_nil {α} : (∅ : StackTape α) = nil := rfl
+
+@[simp, scoped grind =]
+lemma nil_toList {α} : (nil : StackTape α).toList = [] := rfl
+
+/-- Prepend an `Option` to the `StackTape` -/
+@[scoped grind]
+def cons {α} (x : Option α) (xs : StackTape α) : StackTape α :=
+  match x, xs with
+  | none, ⟨[], _⟩ => ⟨[], by grind⟩
+  | none, ⟨hd :: tl, hl⟩ => ⟨none :: hd :: tl, by grind⟩
+  | some a, ⟨l, hl⟩ => ⟨some a :: l, by grind⟩
+
+@[simp, scoped grind =]
+lemma cons_none_nil_toList {α} : (cons none (nil : StackTape α)).toList = [] := by grind
+
+@[simp, scoped grind =]
+lemma cons_some_toList {α} (a : α) (l : StackTape α) :
+    (cons (some a) l).toList = some a :: l.toList := by simp only [cons]
+
+/-- Remove the first element of the `StackTape`, returning the rest -/
+@[scoped grind]
+def tail {α} (l : StackTape α) : StackTape α :=
+  match hl : l.toList with
+  | [] => nil
+  | hd :: t => ⟨t, by grind⟩
+
+/-- Get the first element of the `StackTape`. -/
+@[scoped grind]
+def head {α} (l : StackTape α) : Option α :=
+  match l.toList with
+  | [] => none
+  | h :: _ => h
+
+lemma eq_iff {α} (l1 l2 : StackTape α) : l1 = l2 ↔ l1.head = l2.head ∧ l1.tail = l2.tail := by
+  constructor
+  · grind
+  · intro ⟨hhead, htail⟩
+    cases l1 with | mk as1 h1 =>
+    cases l2 with | mk as2 h2 =>
+    cases as1 <;> cases as2 <;> grind
+
+@[simp]
+lemma head_cons {α} (o : Option α) (l : StackTape α) : (cons o l).head = o := by
+  cases o with
+  | none =>
+    cases l with | mk toList hl =>
+    cases toList <;> grind
+  | some a => grind
+
+@[simp]
+lemma tail_cons {α} (o : Option α) (l : StackTape α) : (cons o l).tail = l := by
+  cases o with
+  | none =>
+    cases l with | mk toList h =>
+    cases toList <;> grind
+  | some a =>
+    simp only [cons, tail]
+
+@[simp]
+lemma cons_head_tail {α} (l : StackTape α) :
+    cons (l.head) (l.tail) = l := by
+  rw [eq_iff]
+  simp
+
+/-- Create a `StackTape` from a list by mapping all elements to `some` -/
+@[scoped grind]
+def map_some {α} (l : List α) : StackTape α := ⟨l.map some, by simp⟩
+
+section Length
+
+/-- The length of the `StackTape` is the number of elements up to the last non-`none` element -/
+@[scoped grind]
+def length {α} (l : StackTape α) : ℕ := l.toList.length
+
+lemma length_tail_le {α} (l : StackTape α) : l.tail.length ≤ l.length := by
+  grind
+
+grind_pattern length_tail_le => l.tail.length
+
+@[scoped grind =]
+lemma length_cons_none {α} (l : StackTape α) :
+    (cons none l).length = l.length + if l.length = 0 then 0 else 1 := by
+  cases l with | mk toList h =>
+  cases toList <;> grind
+
+@[scoped grind =]
+lemma length_cons_some {α} (a : α) (l : StackTape α) : (cons (some a) l).length = l.length + 1 := by
+  grind
+
+lemma length_cons_le {α} (o : Option α) (l : StackTape α) : (cons o l).length ≤ l.length + 1 := by
+  cases o <;> grind
+
+@[simp, scoped grind =]
+lemma length_map_some {α} (l : List α) : (map_some l).length = l.length := by grind
+
+@[simp, scoped grind =]
+lemma length_nil {α} : (nil : StackTape α).length = 0 := by grind
+
+end Length
+
+end StackTape
+
+end Turing