diff --git a/doc/notes.typ b/doc/notes.typ
index 59b1e61..3bc8777 100644
--- a/doc/notes.typ
+++ b/doc/notes.typ
@@ -7,6 +7,7 @@
 #let breakl(b) = {
   raw(b.text.replace(regex(" *\\\\\n *"), " "), lang: b.lang, block: b.block)
 }
+#set raw(syntaxes: "zelus.sublime-syntax")
 
 #show raw: set text(font: "CaskaydiaCove NF")
 #show link: underline
@@ -495,3 +496,71 @@ simulation loop as follows:
   implemented in an imperative language like C. Code generation for hybrid
   models has much in common with code generation for synchronous languages.
 ])
+
+== Miscellaneous
+
+=== Signals
+
+Superdense time defines signals as
+$S u p e r d e n s e(bb(V)) = bb(R) * bb(N) -> bb(V)$, where given
+$f : S u p e r d e n s e(bb(V))$, $f(t, n) = f(t + n partial)$ in the
+non-standard semantics.
+
+Our representation instead uses
+$S i g n a l(bb(V)) = S t r e a m((h : bb(R)) * ([0, h] -> bb(V)))$. Can we 
+convert between the two as we want?
+
+#breakl(```ocaml
+let (@.) f g x = f (g x)
+let splt f g x = f x, g x
+
+type 'a superdense = float * int -> 'a
+type 'a signal     = (float * (float -> 'a)) stream
+
+let h = fst @. hd
+let u = snd @. hd
+
+let compose : 'a signal -> 'a superdense * float stream =
+  let rec g v s n =
+    if n = 0 then v
+    else if h s <> 0. then u s 0.
+    else g (u s 0.) (tl s) (n - 1) in
+  let rec f s = fun (t, n) ->
+    if t < h s then u s t
+    else if t = h s then g (u s t) (tl s) n
+    else f (tl s) (t -. h s, n) in
+  splt f (map fst)
+
+let decompose : 'a superdense * float stream -> 'a signal =
+  let rec f r n = fun (s, h) ->
+    if hd h = 0. then (0., fun _ -> s (r, n)) @: f r (n + 1) (s, tl h)
+    else (hd h, fun t -> s (t +. r, 0)) @: f (r +. hd h) 0 (s, tl h) in
+  f 0. 0
+```)
+
+#pagebreak()
+=== Continuity of assertions
+
+In Zélus, the following program is forbidden:
+
+```zelus
+let hybrid f x = x >= 0
+```
+
+One cannot then write
+```zelus
+let hybrid ball () = y where
+  rec der y  = y'   init y0
+  and der y' = -. g init 0.0 reset z -> (-0.8 *. last y')
+  and     z  = up (-. y)
+  and assert (f y)
+```
+even though we want the following, equivalent program to work:
+```zelus
+let hybrid ball () = y where
+  rec der y  = y'   init y0
+  and der y' = -. g init 0.0 reset z -> (-0.8 *. last y')
+  and     z  = up (-. y)
+  and assert (y >= 0)
+```
+Is this an issue?
diff --git a/doc/pres.typ b/doc/pres.typ
new file mode 100644
index 0000000..5c292c6
--- /dev/null
+++ b/doc/pres.typ
@@ -0,0 +1,868 @@
+#import "@preview/cetz:0.3.2"
+#import "@preview/cetz-plot:0.1.1"
+#import "@preview/finite:0.4.1"
+#import "@preview/touying:0.6.1": *
+#import themes.simple: *
+
+// TODO: clarify between
+// `solver.step : time * 's -> (time * (time -> 'y) * zin option) * 's`
+// and `sim.step : (time * (time -> 'a)) * 's -> (time * (time -> 'b)) * 's`
+
+#show: simple-theme.with(
+  aspect-ratio: "16-9",
+  config-common(show-bibliography-as-footnote: bibliography("sources.bib")),
+)
+#let cetz-canvas = touying-reducer.with(
+  reduce: cetz.canvas,
+  cover: cetz.draw.hide.with(bounds: true)
+)
+#let arrow(start, ..steps, stroke: black) = cetz.draw.line(
+  ..(steps.pos().fold((start,), (acc, step) => {
+    let ((.., (x, y)), (d, l)) = (acc, step)
+    let (nx, ny) = if d == "d" {
+      (x, y - l)
+    } else if d == "u" {
+      (x, y + l)
+    } else if d == "l" {
+      (x - l, y)
+    } else if d == "r" {
+      (x + l, y)
+    } else {
+      (x, y)
+    }
+    acc.push((nx, ny))
+    acc
+  })),
+  mark: (end: "straight"),
+  stroke: stroke
+)
+#let (d, u, l, r) = ("d", "u", "l", "r")
+#let box(start, dim, double: false, content: none, ..rest) = {
+  let (x, y) = start
+  let (dx, dy) = dim
+  cetz.draw.rect((x, y), (x + dx, y + dy), ..rest)
+  if double {
+    cetz.draw.rect((x + 0.1, y + 0.1), (x + dx - 0.1, y + dy - 0.1), ..rest)
+  }
+  if content != none {
+    cetz.draw.content((x + dx / 2, y + dy / 2), content)
+  }
+}
+#set raw(syntaxes: "zelus.sublime-syntax")
+#show raw: set text(font: "CaskaydiaCove NF")
+
+#let rbrace(in-block, out-block, out-width: auto, ..args) = {
+  math.lr([
+    #in-block
+    $mid(})$
+    #block(width: out-width, out-block)
+  ])
+}
+
+= Executing Hybrid Systems
+
+Henri Saudubray
+#footnote(link("https://codeberg.org/17maiga/hsim"), numbering: "*")
+
+22/05/2025
+
+
+= Hybrid Systems <touying:hidden>
+
+== Hybrid systems, as seen in Zélus
+
+Computation alternates between _discrete_ and _continuous_ phases.
+#pause #linebreak()
+Use of an ODE solver to approximate continuous behaviour.
+#pause #linebreak()
+Side effects and state jumps occur in discrete steps triggered by
+zero-crossings.
+
+#meanwhile
+
+#align(horizon, {
+  columns(2, [
+    ```zelus
+    let hybrid saw() = y where
+      rec der y = 1.0
+          init 0.0
+          reset z -> (0.0)
+      and z = up(y -. 1.0)
+    ```
+    #align(center, {
+      import cetz: *
+      import cetz-plot.plot: *
+      canvas({
+        plot(
+          size: (9, 4), axis-style: "school-book", legend: (7.25, 4.5),
+          x-tick-step: 1, x-label: none, y-tick-step: 1, y-label: none,
+          y-grid: true, y-min: -0.5, y-max: 1.5, x-min: 0, x-max: 4.5,
+          plot-style: (stroke: blue), {
+          for i in range(5) {
+            add(((i, 0), (i + 1, 1)))
+          }
+          add(((0, 0),), label: [`saw`])
+        })
+      })
+    })
+  ])
+})
+
+== Hybrid assertions
+
+Assertions are themselves hybrid systems.
+#pause #linebreak()
+Adding assertions can change the final result, they are not _transparent_.
+#pause #linebreak()
+Solution: simulate assertions with their own solver.
+#meanwhile
+
+#columns(2, [
+  #align(horizon, [
+    ```zelus
+    let hybrid saw() = y where
+      rec der y = 1.0
+          init 0.0
+          reset z -> (0.0)
+      and z = up(y -. 1.0)
+      and assert(0.0 <= y <= 1.0)
+    ```
+  ])
+  #colbreak()
+  #align(center + horizon, {
+    import cetz: *
+    canvas({
+      import cetz.draw: *
+      box((0, 0), (8, 4.5))
+      box((2, 0.25), (4, 1.5), content: ```zelus assert```)
+      box((2, 2.75), (4, 1.5), content: `...`)
+      arrow((-1, 3.5), (r, 3))
+      arrow((6, 3.5), (r, 3))
+      arrow((7, 3.5), (d, 1.25), (l, 6), (d, 1.25), (r, 1))
+      content((-1.5, 3.5), [`()`])
+      content((9.5, 3.5), [`y`])
+      content((1, 5), [`saw`])
+    })
+  })
+])
+
+= Nodes <touying:hidden>
+
+== Discrete nodes
+
+Nodes take an additional reset parameter `'p` for their reset function:
+
+#align(horizon)[
+  #grid(columns: (3fr, 2fr), align: (left, left), 
+  ```ocaml
+  type ('p, 'a, 'b) dnode =
+    DNode : {
+      state : 's;
+      step  : 's -> 'a -> 'b * 's;
+      reset : 'p -> 's -> 's;
+    } -> ('p, 'a, 'b) dnode
+  ```,
+  cetz.canvas({
+    import cetz.draw: *
+    box((0, 0), (4, 4), content: `DNode`)
+    arrow((-1, 2), (r, 1))
+    arrow((4, 2), (r, 1))
+    arrow((2, 5), (d, 1))
+    content((-1.6, 2), `'a`)
+    content((5.6, 2), `'b`)
+    content((2, 5.6), `'p`)
+  }))
+]
+
+== Hybrid nodes
+
+Hybrid nodes are a bit more complex:
+#block([
+  ```ocaml
+  type ('p, 'a, 'b, 'y, 'yder, 'zin, 'zout) hnode =
+    HNode : {
+      state : 's;
+      step  : 's -> 'a -> 'b * 's;
+      reset : 'p -> 's -> 's;
+      fder  : 's -> 'a -> 'y -> 'yder;
+      fzer  : 's -> 'a -> 'y -> 'zout;
+      fout  : 's -> 'a -> 'y -> 'b;
+      (* ... *)
+    } -> ('p, 'a, 'b, 'y, 'yder, 'zin, 'zout) hnode
+  ```
+  #pause
+  #place(left + top, dx: 75%, dy: 36%, block(grid(
+    align: left + horizon, columns: (1fr, 10fr),
+    move(scale(y: 200%, $}$), dy: -2%), [Discrete behaviour]
+  ), width: 40%))
+  #place(left + top, dx: 75%, dy: 62.5%, block(grid(
+    align: left + horizon, columns: (1fr, 10fr),
+    move(scale(y: 300%, $}$), dy: -2%), [Continuous behaviour]
+  ), width: 40%))
+])
+
+= Solvers are nodes <touying:hidden>
+
+== ODE solvers
+
+#slide(self => [
+  #let (uncover, only) = utils.methods(self)
+
+  ODE solvers are discrete nodes producing streams of functions defined on 
+  successive intervals:
+  $(h: bb(R)_+) -->^D (h': bb(R)_+) times (u: [0,h'] -> bb(V))$.
+
+  #linebreak()
+  #grid(columns: (1fr, 1fr), align: (center, left), cetz.canvas({
+    import cetz.draw: *
+    box((0, 0), (4, 4), content: `csolver`)
+    arrow((-1, 2), (r, 1))
+    arrow((4, 3), (r, 1))
+    arrow((4, 1), (r, 1))
+    content((-1.5, 2), $h$)
+    content((5.5, 3), $h'$)
+    content((5.5, 1), $u$)
+    arrow((2, 5), (d, 1))
+    content((2, 5.6), "IVP")
+  }), align(horizon, cetz-canvas({
+    import cetz-plot.plot: *
+    only(1, plot(
+      size: (10, 4.5), axis-style: "school-book", legend: (9, 4.5),
+      y-tick-step: none, y-label: none, y-min: 0, y-max: 6,
+      x-tick-step: none, x-label: none, x-min: 0, x-max: 5,
+      x-ticks: ((5, $h$), (2, $h'$)), {
+      add(domain: (0, 2), t => calc.sin(t) + t, label: $u$)
+    }))
+    only(2, plot(
+      size: (10, 4.5), axis-style: "school-book", legend: (9, 4.5),
+      y-tick-step: none, y-label: none, y-min: 0, y-max: 6,
+      x-tick-step: none, x-label: none, x-min: 0, x-max: 5,
+      x-ticks: ((5, $h$), (2, ""), (4, $h'$)), {
+      add(domain: (2, 4), t => calc.sin(t) + t, label: $u$)
+      add(domain: (0, 2), t => calc.sin(t) + t)
+    }))
+    only(3, plot(
+      size: (10, 4.5), axis-style: "school-book", legend: (9, 4.5),
+      y-tick-step: none, y-label: none, y-min: 0, y-max: 6,
+      x-tick-step: none, x-label: none, x-min: 0, x-max: 5,
+      x-ticks: ((2, ""), (4, ""), (5, $h, h'$)), {
+      add(domain: (4, 5), t => calc.sin(t) + t, label: $u$)
+      add(domain: (0, 4), t => calc.sin(t) + t)
+    }))
+  })))
+])
+
+== Zero-crossing solvers
+
+#slide(self => [
+  #let (uncover, only) = utils.methods(self)
+
+  Zero-crossing solvers are discrete nodes too, looking for zero-crossings on 
+  functions:
+  $(h: bb(R)_+) times (u: [0, h] -> bb(V)) -->^D
+   (h': bb(R)_+) times (z: bb(Z)?)$.
+
+  #linebreak()
+  #grid(columns: (1fr, 1fr), align: (center, left), cetz.canvas({
+    import cetz.draw: *
+    box((0, 0), (4, 4), content: `zsolver`)
+    arrow((-1, 1), (r, 1))
+    arrow((-1, 3), (r, 1))
+    arrow((4, 1),  (r, 1))
+    arrow((4, 3),  (r, 1))
+    arrow((2, 5),  (d, 1))
+    content((-1.5, 3), $h$)
+    content((-1.5, 1), $u$)
+    content((5.5, 3), $h'$)
+    content((5.5, 1), $z$)
+    content((2, 5.6), "ZC")
+  }), align(horizon, cetz-canvas({
+    import cetz-plot.plot: *
+    only(1, plot(
+      size: (10, 4.5), axis-style: "school-book", legend: (9, 4.5),
+      y-tick-step: none, y-label: none, y-min: -2, y-max: 5,
+      x-tick-step: none, x-label: none, x-min: 0, x-max: 2,
+      x-ticks: ((2/3, $h, h'$),), {
+      add(domain: (0, 2/3), t => t * t - 1, label: "u")
+    }))
+    only(2, plot(
+      size: (10, 4.5), axis-style: "school-book", legend: (9, 4.5),
+      y-tick-step: none, y-label: none, y-min: -2, y-max: 5,
+      x-tick-step: none, x-label: none, x-min: 0, x-max: 2,
+      x-ticks: ((1, $h'$), (4/3, $h$)), {
+      add(domain: (2/3, 4/3), t => t * t - 1, label: "u")
+      add(domain: (0, 2/3), t => t * t - 1)
+    }))
+    only(3, plot(
+      size: (10, 4.5), axis-style: "school-book", legend: (9, 4.5),
+      y-tick-step: none, y-label: none, y-min: -2, y-max: 5,
+      x-tick-step: none, x-label: none, x-min: 0, x-max: 2,
+      x-ticks: ((2, $h, h'$),), {
+      add(domain: (1, 2), t => t * t - 1, label: "u")
+      add(domain: (0, 1), t => t * t - 1)
+    }))
+    only("1, 3", cetz.draw.content((2, 4), $z = bot$))
+    only("2", cetz.draw.content((2, 3.9), $z != bot$))
+  })))
+])
+
+== A full solver
+
+Combine an ODE solver `csolver` with a zero-crossing solver `zsolver`:
+
+#linebreak()
+
+#align(center, {
+  import cetz: *
+  canvas({
+    import cetz.draw: *
+    box((0, 0), (12, 4))
+    content((1.5, 4.5), `solver`)
+    box((1, 0.5), (4, 3), content: `csolver`)
+    box((7, 1.5), (4, 2), content: `zsolver`)
+    arrow((-1, 2), (r, 2))
+    arrow((5, 3), (r, 2))
+    arrow((5, 1), (r, 8))
+    arrow((6, 1), (u, 1), ("r", 1))
+    arrow((11, 2), (r, 2))
+    arrow((11, 3), (r, 2))
+    content((-1.5, 2), [$h$])
+    content((6, 3.5), [$h'$])
+    content((6, 0.5), [$u$])
+    content((13.5, 1), [$u$])
+    content((13.75, 2), [$h''$])
+    content((13.5, 3), [$z$])
+  })
+})
+
+= Signals <touying:hidden>
+
+== Semantics
+
+Two semantics are often used for hybrid systems:
+- Superdense semantics @opsem_lee_zheng:
+  - signals are functions from $bb(R) times bb(N) -> bb(V)$;
+  - discrete instants are ordered lexicographically
+- Non-standard semantics @ns_sem_benveniste_bourke_caillaud_pouzet:
+  - signals are functions from the hyperreals $""^*bb(R) -> bb(V)$;
+  - discrete instants are ordered using infinitesimals
+
+== Optional values
+
+The solver does not always reach the requested horizon in a single step.
+#linebreak()
+We _wait_ for it to finish computing:
+
+#align(center, {
+  import cetz: *
+  canvas({
+    import cetz.draw: *
+    content((0, 1.5), "Input:")
+    content((0, 0), "Output:")
+    content((3.5, 1.5), $a_0,$)
+    content((3.5, 0), $bot,$)
+    content((5, 1.5), $bot,$)
+    content((5, 0), $b_0,$)
+    content((6.5, 1.5), $bot,$)
+    content((6.5, 0), $b_1,$)
+    content((8, 1.5), $bot,$)
+    content((8, 0), $b_2,$)
+    content((9.5, 1.5), $bot,$)
+    content((9.5, 0), $bot,$)
+    content((11, 1.5), $a_2,$)
+    content((11, 0), $bot,$)
+    content((12.5, 1.5), $bot,$)
+    content((12.5, 0), $b_3,$)
+    content((14, 1.5), $bot,$)
+    content((14, 0), $b_4,$)
+    content((15.5, 1.5), $...$)
+    content((15.5, 0), $...$)
+  })
+})
+
+This is represented by optional values:
+
+$ "Signal"(alpha) = "Stream"("Optional"((h:bb(R)_+) times ([0,h] -> alpha))) $
+
+== Discrete instants
+
+Discrete instants are represented by constant functions of length 0. Their
+order is the order of apparition in the stream.
+
+== Example
+
+The stream
+#align(center, ```ocaml
+f = (1.0, λt -> t)::(0.0, λt -> 2.0)::(0.3, λt -> 3*t)::...
+```)
+defines the function $f : ""^*bb(R)_+ -> bb(R)$
+#grid(columns: (1fr, 1fr), align: (center, center), $ & f(t) = cases(
+  "st"(t)#footnote([
+    $"st"(t)$ denotes the _standard part_ of $t$, that is, the closest real
+    number $r$ to $t$.
+  ]) & "if" t in [0, 1],
+  2        & "if" t = 1 + partial,
+  3 dot "st"(t) & "if" t in [1 + 2 partial, 1.3],
+  ...
+) $, cetz.canvas({
+  import cetz-plot.plot: *
+  plot(
+    size: (10, 3), axis-style: "school-book",
+    y-label: none, y-tick-step: none,
+    x-label: none, x-tick-step: none, x-ticks: (1, 2.3), x-grid: true,
+    {
+      add(domain: (0, 1), t => t)
+      add(((1, 2),), mark: "o", mark-size: 0.05,
+       mark-style: (stroke: blue, fill: blue))
+      add(domain: (1, 1.3), t => 3 * t, style: (stroke: blue))
+    }
+  )
+}))
+
+= Simulation <touying:hidden>
+
+== Simulation
+
+The simulation is itself a discrete node on signals:
+
+#align(center, cetz.canvas({
+  import cetz.draw: *
+  box((0, 0), (12, 5), content: `???`)
+  arrow((-1, 2.5), (r, 1))
+  arrow((12, 2.5), (r, 1))
+  content((-3, 2.5), $"Signal"(alpha)$)
+  content((15, 2.5), $"Signal"(beta)$)
+  content((1, 5.5), `sim`)
+  box((0.5, 0.5), (4, 4), content: `model`)
+  box((7.5, 0.5), (4, 4), content: `solver`)
+}))
+
+It runs according to one of two modes: _discrete_ and _continuous_.
+
+== (Re)initialization
+
+When receiving a new value, store it
+#alternatives([...], [and reset the solver.])
+#align(center, cetz-canvas({
+  import cetz.draw: *
+
+  // sim
+  content((1, 6.5), `sim`)
+  box((0, 0), (14, 6))
+
+  // model
+  content((2.5, 5.25), `model`)
+  box((1, 1), (4, 3.75))
+
+  // model.fzer
+  box((1.25, 3), (3.5, 1.5), content: `fzer`)
+
+  // model.fder
+  box((1.25, 1.25), (3.5, 1.5), content: `fder`)
+
+  // sim state
+  box((10, 1.25), (3, 1.5), double: true, content: `state`)
+
+  // (h, u) -> state
+  content((-2.25, 3), $(h, u)$) 
+  arrow((-1, 3), (r, 1.5), (d, 2.5), (r, 5), (u, 1.5), (r, 4.5))
+
+  // sim -> bot
+  arrow((14, 3), (r, 1))
+  content((15.5, 3), $bot$)
+
+  (pause,)
+
+  // computation
+  box((6, 3), (3, 1.5), content: `...`)
+
+  // solver
+  box((10, 3), (3, 1.5), content: `solver`)
+
+  // (h, u) -> computation
+  arrow((5.5, 2), (u, 1.5), (r, 0.5))
+
+  // fzer -> computation
+  arrow((4.75, 4), (r, 1.25))
+
+  // fder -> computation
+  arrow((4.75, 2), (r, 0.5), (u, 1.75), (r, 0.75))
+
+  // computation -> solver
+  arrow((9, 3.75), (r, 0.5), (u, 1.25), (r, 2), (d, 0.5))
+  content((10.5, 5.5), `ivp + zc`)
+}))
+
+== Discrete step
+
+#alternatives(
+  [Use the model's `step` function and the stored input.],
+  [Build a constant function out of the output value.],
+  [Update the running mode as needed.]
+)
+#align(center, cetz-canvas({
+  import cetz.draw: *
+  // sim
+  content((1, 6.5),  `sim`)
+  box((0, 0), (17, 6))
+
+  // sim state
+  box((1, 1), (3, 1.5), double: true, content: `state`)
+
+  // model
+  content((6.5, 5.5),  `model`)
+  box((5, 0.5), (7, 4.5))
+
+  // model step
+  box((7, 1), (3, 1.5), content: `step`)
+
+  // model state
+  box((7, 2.75), (3, 1.5), double: true, content: `state`)
+
+  // bot -> sim
+  arrow((-1, 3), (r, 1))
+  content((-1.5, 3), $bot$)
+
+  // sim.state -> model.step
+  arrow((4, 1.5), (r, 3))
+  content((5.75, 1.25), $alpha$)
+
+  // model.state -> model.step
+  arrow((7, 3.5), (l, 0.5), (d, 1.5), (r, 0.5))
+  content((6, 2.875), $sigma$)
+
+  (pause,)
+
+  // constant signal
+  box((13, 1), (3, 1.5), content: `...`)
+
+  // model.step -> model.state
+  arrow((10, 2), (r, 0.5), (u, 1.5), (l, 0.5))
+  content((11, 2.875), $sigma$)
+
+  // model.step -> ...
+  arrow((10, 1.5), (r, 3))
+  content((11.25, 1), $beta$)
+
+  // constant signal -> signal(beta)
+  arrow((16, 1.75), (r, 0.5), (u, 1.25), (r, 1.5))
+  content((20, 3), $"Signal"(beta)$)
+
+  (pause,)
+
+  // computation for mode
+  box((1, 3.5), (3, 1.5), content: `...`)
+
+  // model.step -> mode computations
+  arrow((10.5, 3.5), (u, 1), (l, 6.5))
+
+  // sim.state -> mod.computations
+  arrow((4, 2), (r, 0.5), (u, 2), (l, 0.5))
+
+  // mod.computations -> sim.state
+  arrow((1, 4.25), (l, 0.5), (d, 2.5), (r, 0.5))
+}))
+
+== Continuous step
+
+#alternatives(
+  [Call the solver with the current target horizon.],
+  [Use the current input and the result of the solver to build the output.],
+  [Update the model's continuous state with the new horizon.],
+  [Update the simulation mode in case of a zero-crossing.],
+)
+
+#align(center, cetz-canvas({
+  import cetz.draw: *
+  // sim
+  content((1, 6.5), `sim`)
+  box((0, 0), (17, 6))
+
+  // sim.state
+  box((1, 1), (3, 1.5), double: true, content: `state`)
+
+  // bot -> sim
+  arrow((-1, 3), (r, 1))
+  content((-1.5, 3), $bot$)
+
+  // solver
+  content((6.5, 5.25), `solver`)
+  box((5, 0.75), (6, 4))
+
+  // solver.step
+  box((6.5, 1), (3, 1.5), content: `step`)
+  
+  // solver.state
+  box((6.5, 2.75), (3, 1.5), double: true, content: `state`)
+
+  // solver.state -> solver.step
+  arrow((6.5, 3.5), (l, 0.5), (d, 1.5), (r, 0.5))
+  content((5.5, 2.75), $sigma$)
+
+  // sim.state -> solver.step
+  arrow((4, 1.5), (r, 2.5))
+
+  (pause,)
+
+  // solver.step -> solver.state
+  arrow((9.5, 2.2), (r, 0.5), (u, 1.3), (l, 0.5))
+
+  // computation
+  box((13, 1), (3, 1.5), content: `...`)
+
+  // solver.step -> computation
+  arrow((9.5, 1.6), (r, 3.5))
+  arrow((9.5, 1.3), (r, 3.5))
+
+  // sim.state -> computation
+  arrow((4, 2), (r, 0.5), (d, 1.5), (r, 8), (u, 1.55), (r, 0.5))
+
+  // computation -> beta signal
+  arrow((16, 1.75), (r, 2.5))
+  content((20.5, 1.75), $"Signal"(beta)$)
+
+  (pause,)
+
+  // model
+  box((12.5, 2.75), (4, 2))
+  content((14, 5.25), `model`)
+
+  // model.state
+  box((13, 3), (3, 1.5), double: true, content: `state`)
+
+  // step -> model
+  arrow((12.25, 1.3), (u, 2.2), (r, 0.75))
+  arrow((12, 1.6), (u, 2.4), (r, 1))
+
+  (pause,)
+
+  // computation
+  box((1, 2.75), (3, 1.5), content: `...`)
+
+  // solver.step -> computation
+  arrow((9.5, 1.9), (r, 1), (u, 2.6), (l, 6), (d, 1), (l, 0.5))
+
+  // computation -> solver.state
+  arrow((1, 3.5), (l, 0.5), (d, 1.75), (r, 0.5))
+}))
+#pause
+Is that it?
+
+= States <touying:hidden>
+
+== The state problem
+
+#slide(self => [
+  #let (uncover, only) = utils.methods(self)
+  Some solvers modify their state in-place (e.g. #smallcaps("Sundials")).
+  #linebreak()
+  The function returned depends on this state.
+  #pause #linebreak()
+  It becomes invalid once we call the solver again.
+
+  #meanwhile
+  #align(center, cetz-canvas({
+    import cetz-plot.plot: *
+    plot(
+      size: (10, 4), axis-style: "school-book",
+      x-label: none, x-tick-step: none, x-max: 6,
+      y-label: none, y-tick-step: none, y-max: 6,
+      x-grid: true, x-ticks: ((4.5, ""),),
+      {
+        only(1, add(domain: (0, 4.5), t => calc.sin(t) + t))
+        only(2, add(domain: (4.5, 6), t => calc.sin(t) + t))
+        only(2, add(domain: (0, 4.5), t => calc.sin(t) + t))
+      }
+    )
+  }))
+])
+
+== Solver steps
+
+Most solvers start off with smaller steps, and increase the step length
+progressively.
+
+#align(center, cetz.canvas({
+  import cetz-plot.plot: *
+  plot(
+    size: (10, 4), axis-style: "school-book", x-label: none, x-tick-step: none,
+    x-ticks: ((0,""), (0.001,""), (0.01,""), (0.1,""), (0.2,""), (0.4,""),
+              (1,""), (1.9,""), (3.9, "")), x-grid: true,
+    y-label: none, y-tick-step: none, {
+      add(domain: (0, 6), t => calc.sin(t) + t)
+    }
+  )
+}))
+
+Combined with in-place state modifications and resets, this could hinder
+performance.
+
+== State copies
+
+Copying (part of) the state solves this issue.
+#linebreak()
+If the solver supports state copies, we can call it more than once per
+simulation step.
+
+```ocaml
+type ('p, 'a, 'b) dnode_c =
+  DNodeC : {
+    state : 's;
+    step  : 's -> 'a -> 'b * 's;
+    reset : 'p -> 's -> 's;
+    copy  : 's -> 's;
+  } -> ('p, 'a, 'b) dnode_c
+```
+
+== Accelerating the simulation
+
+We can then concatenate functions obtained from successive continuous steps.
+If no zero-crossing is found, there is no discontinuity.
+
+#linebreak()
+
+#grid(align: center + horizon, columns: (10fr, 1fr, 10fr),
+  cetz.canvas({
+    import cetz-plot.plot: *
+    plot(
+      size: (8, 4), axis-style: "school-book", x-label: none,
+      x-tick-step: none, x-ticks: ((3, $h_1$), (6, $h_2$)), x-grid: true,
+      y-label: none, y-tick-step: none, {
+        add(domain: (0, 3), t => calc.sin(t) + t)
+        add(domain: (3, 6), t => calc.sin(t) + t)
+      }
+    )
+  }), $==>$, cetz.canvas({
+        import cetz-plot.plot: *
+    plot(
+      size: (8, 4), axis-style: "school-book", x-label: none,
+      x-tick-step: none, x-ticks: ((6, $h_1$),), x-grid: true, y-label: none,
+      y-tick-step: none, { add(domain: (0, 6), t => calc.sin(t) + t) }
+    )
+  })
+)
+
+= Composing simulations <touying:hidden>
+
+== Pushing values through
+
+#slide(self => [
+  #let (uncover, only) = utils.methods(self)
+
+  Unless we can copy the state, we need to use up all of a value before
+  producing the next. We need to push empty values ($bot$) as needed.
+
+  #align(center, cetz-canvas({
+    import cetz.draw: *
+    box((0, 0), (3, 3), content: $M_1$)
+    box((8, 0), (3, 3), content: $M_2$)
+    only("1, 3-4", arrow((-1, 1.5), (r, 1)))
+    only("2, 5-", arrow((-1, 1.5), (r, 1), stroke: red))
+    only("1, 2, 4-", arrow((3, 1.5), (r, 5)))
+    only("3", arrow((3, 1.5), (r, 5), stroke: red))
+    only("-3", arrow((11, 1.5), (r, 1)))
+    only("4-", arrow((11, 1.5), (r, 1), stroke: red))
+    content((-3, 1.5), $"Signal"(alpha)$)
+    content((5.5, 2), $"Signal"(beta)$)
+    content((14, 1.5), $"Signal"(gamma)$)
+  
+    content((-4, -1),   $alpha:$)
+    content((-4, -2.5), $beta:$)
+    content((-4, -4),   $gamma:$)
+    (pause,)
+    content((-2, -4), $bot$)
+    content((-2, -2.5), $bot$)
+    content((-2, -1.1), $alpha_1$)
+    (pause,)
+    content((0, -1), $bot$)
+    content((0, -2.6), $beta_1$)
+    content((0, -4), $bot$)
+    (pause,)
+    content((2, -1), $bot$)
+    content((2, -2.5), $bot$)
+    content((2, -4.1), $gamma_1$)
+    (pause,)
+    content((4, -1.1), $alpha_2$)
+    content((4, -2.5), $bot$)
+    content((4, -4.1), $gamma_2$)
+    content((5.5, -1), $...$)
+    content((5.5, -2.5), $...$)
+    content((5.5, -4), $...$)
+    (pause,)
+    box((3.5, -3), (1, 1), stroke: red)
+    box((0.1, 0.1), (2.8, 2.8), stroke: red)
+    content((12, -2.6), "Possible early reset!")
+  }))
+])
+
+== Pulling values from
+
+#slide(self => [
+  #let (uncover, only) = utils.methods(self)
+
+  The output signal stops at least as often as the input signal does.
+  #linebreak()
+  This calls for a "lazy" composition: we request rather than provide data.
+  
+  #align(center, cetz-canvas({
+    import cetz.draw: *
+    box((0, 0), (3, 3), content: $M_1$)
+    box((8, 0), (3, 3), content: $M_2$)
+    only("1-3, 5-10, 12-", arrow((-1, 1.5), (r, 1)))
+    only("4, 11", arrow((-1, 1.5), (r, 1), stroke: red))
+    only("1-2, 4-5, 7-8, 10-11, 13-", arrow((3, 1.5), (r, 5)))
+    only("3, 6, 9, 12", arrow((3, 1.5), (r, 5), stroke: red))
+    only("1, 3-4, 6, 9, 11-12, 14-", arrow((11, 1.5), (r, 1)))
+    only("2, 5, 7, 8, 10, 13", arrow((11, 1.5), (r, 1), stroke: red))
+    content((-3, 1.5), $"Signal"(alpha)$)
+    content((5.5, 2), $"Signal"(beta)$)
+    content((14, 1.5), $"Signal"(gamma)$)
+  
+    content((-4, -1), $alpha:$)
+    content((-4, -2.5), $beta:$)
+    content((-4, -4), $gamma:$)
+    (pause,)
+    content((-2, -4), $bot$)
+    (pause,)
+    content((-2, -2.5), $bot$)
+    (pause,)
+    content((-2, -1.1), $alpha_1$)
+    (pause,)
+    content((0, -4), $bot$)
+    (pause,)
+    content((0, -2.6), $beta_1$)
+    (pause,)
+    content((2, -4.1), $gamma_1$)
+    (pause,)
+    content((4, -4.1), $gamma_2$)
+    (pause,)
+    content((6, -2.6), $beta_2$)
+    content((6, -4), $bot$)
+    (pause,)
+    content((8, -4.1), $gamma_3$)
+    (pause,)
+    content((10, -4), $bot$)
+    content((10, -2.5), $bot$)
+    content((10, -1.1), $alpha_2$)
+    (pause,)
+    content((12, -2.6), $beta_3$)
+    content((12, -4), $bot$)
+    (pause,)
+    content((14, -4.1), $gamma_4$)
+    (pause,)
+    content((15.5, -1), $...$)
+    content((15.5, -2.5), $...$)
+    content((15.5, -4), $...$)
+  }))
+])
+
+= Conclusion <touying:hidden>
+
+== What next?
+
+#align(horizon, [
+  - Can we avoid pointless solver resets?
+  - Think about assertions: is the checking of an assertion a composition?
+  - Plug to Zélus' output
+])
+
diff --git a/doc/sources.bib b/doc/sources.bib
new file mode 100644
index 0000000..afd15fa
--- /dev/null
+++ b/doc/sources.bib
@@ -0,0 +1,16 @@
+@article{
+  ns_sem_benveniste_bourke_caillaud_pouzet,
+  title={Non-Standard Semantics of Hybrid Systems Modelers},
+  author={Benveniste, Albert and Bourke, Timothy and
+          Caillaud, Benoıt and Pouzet, Marc},
+  year={2011},
+  language={en}
+}
+@inbook{
+  opsem_lee_zheng,
+  title={Operational Semantics of Hybrid Systems},
+  ISBN={978-3-540-25108-8},
+  author={Lee, Edward A. and Zheng, Haiyang},
+  year={2005},
+  language={en}
+}
diff --git a/doc/zelus.sublime-syntax b/doc/zelus.sublime-syntax
new file mode 100644
index 0000000..f67a028
--- /dev/null
+++ b/doc/zelus.sublime-syntax
@@ -0,0 +1,36 @@
+%YAML 1.2
+---
+name: Zelus
+file_extensions: [zls, zli]
+scope: source
+
+contexts:
+  main:
+    - match: \b(let|in|where|rec|and|local)\b
+      scope: keyword.control
+
+    - match: \b(if|then|else)\b
+      scope: keyword.control.conditional
+
+    - match: \b(hybrid|node)\b
+      scope: keyword.control
+
+    - match: \b(up|assert|der|init|reset|last)\b
+      scope: entity.name.constant
+
+    - match: '"'
+      push: string
+    - match: \(\*
+      push: comment
+
+  string:
+    - meta_scope: string.quoted.double
+    - match: \\.
+      scope: constant.character.escape
+    - match: '"'
+      pop: true
+
+  comment:
+    - meta_scope: comment
+    - match: \*\)
+      pop: true