diff --git a/argus-semantics/src/eval.rs b/argus-semantics/src/eval.rs
index 1553f79..e69de29 100644
--- a/argus-semantics/src/eval.rs
+++ b/argus-semantics/src/eval.rs
@@ -1,61 +0,0 @@
-use argus_core::expr::*;
-use argus_core::signals::traits::{SignalAbs, TrySignalCast};
-use argus_core::signals::Signal;
-use argus_core::ArgusResult;
-use num_traits::{Num, NumCast};
-
-use crate::Trace;
-
-pub fn eval_num_expr<T>(root: &NumExpr, trace: &impl Trace) -> ArgusResult<Signal<T>>
-where
-    T: Num + NumCast,
-    Signal<i64>: TrySignalCast<Signal<T>>,
-    Signal<u64>: TrySignalCast<Signal<T>>,
-    Signal<f64>: TrySignalCast<Signal<T>>,
-    for<'a> &'a Signal<T>: std::ops::Neg<Output = Signal<T>>,
-    for<'a> &'a Signal<T>: std::ops::Add<&'a Signal<T>, Output = Signal<T>>,
-    for<'a> &'a Signal<T>: std::ops::Sub<&'a Signal<T>, Output = Signal<T>>,
-    for<'a> &'a Signal<T>: std::ops::Mul<&'a Signal<T>, Output = Signal<T>>,
-    for<'a> &'a Signal<T>: std::ops::Div<&'a Signal<T>, Output = Signal<T>>,
-    Signal<T>: SignalAbs,
-{
-    match root {
-        NumExpr::IntLit(val) => Signal::constant(val.0).try_cast(),
-        NumExpr::UIntLit(val) => Signal::constant(val.0).try_cast(),
-        NumExpr::FloatLit(val) => Signal::constant(val.0).try_cast(),
-        NumExpr::IntVar(IntVar { name }) => trace.get::<i64>(name.as_str()).unwrap().try_cast(),
-        NumExpr::UIntVar(UIntVar { name }) => trace.get::<u64>(name.as_str()).unwrap().try_cast(),
-        NumExpr::FloatVar(FloatVar { name }) => trace.get::<f64>(name.as_str()).unwrap().try_cast(),
-        NumExpr::Neg(Neg { arg }) => eval_num_expr(arg, trace).map(|sig| -&sig),
-        NumExpr::Add(Add { args }) => {
-            let mut ret: Signal<T> = Signal::<T>::zero();
-            for arg in args.iter() {
-                let arg = eval_num_expr(arg, trace)?;
-                ret = &ret + &arg;
-            }
-            Ok(ret)
-        }
-        NumExpr::Sub(Sub { lhs, rhs }) => {
-            let lhs = eval_num_expr(lhs, trace)?;
-            let rhs = eval_num_expr(rhs, trace)?;
-            Ok(&lhs - &rhs)
-        }
-        NumExpr::Mul(Mul { args }) => {
-            let mut ret: Signal<T> = Signal::<T>::one();
-            for arg in args.iter() {
-                let arg = eval_num_expr(arg, trace)?;
-                ret = &ret * &arg;
-            }
-            Ok(ret)
-        }
-        NumExpr::Div(Div { dividend, divisor }) => {
-            let dividend = eval_num_expr(dividend, trace)?;
-            let divisor = eval_num_expr(divisor, trace)?;
-            Ok(&dividend / &divisor)
-        }
-        NumExpr::Abs(Abs { arg }) => {
-            let arg = eval_num_expr(arg, trace)?;
-            Ok(arg.abs())
-        }
-    }
-}
diff --git a/argus-semantics/src/lib.rs b/argus-semantics/src/lib.rs
index c5fc33b..4ec374e 100644
--- a/argus-semantics/src/lib.rs
+++ b/argus-semantics/src/lib.rs
@@ -4,9 +4,8 @@
 //! traces_, i.e., a collection of signals that have been extracted from observing and
 //! sampling from some system.
 
-// pub mod eval;
-// pub mod semantics;
-// pub mod traits;
+pub mod semantics;
+pub mod traits;
 pub mod utils;
 
-// pub use traits::{BooleanSemantics, QuantitativeSemantics, Trace};
+pub use traits::Trace;
diff --git a/argus-semantics/src/semantics/boolean.rs b/argus-semantics/src/semantics/boolean.rs
index 35c5ee9..d61ac20 100644
--- a/argus-semantics/src/semantics/boolean.rs
+++ b/argus-semantics/src/semantics/boolean.rs
@@ -3,88 +3,93 @@ use std::time::Duration;
 
 use argus_core::expr::*;
 use argus_core::prelude::*;
+use argus_core::signals::interpolation::Linear;
+use argus_core::signals::SignalPartialOrd;
 
-use crate::traits::{BooleanSemantics, QuantitativeSemantics, Trace};
+use crate::semantics::QuantitativeSemantics;
+use crate::traits::Trace;
+use crate::utils::lemire_minmax::MonoWedge;
 
-impl BooleanSemantics for BoolExpr {
-    fn eval(&self, trace: &impl Trace) -> ArgusResult<Signal<bool>> {
-        match self {
-            BoolExpr::BoolLit(sig) => BooleanSemantics::eval(sig, trace),
-            BoolExpr::BoolVar(sig) => BooleanSemantics::eval(sig, trace),
-            BoolExpr::Cmp(sig) => BooleanSemantics::eval(sig, trace),
-            BoolExpr::Not(sig) => BooleanSemantics::eval(sig, trace),
-            BoolExpr::And(sig) => BooleanSemantics::eval(sig, trace),
-            BoolExpr::Or(sig) => BooleanSemantics::eval(sig, trace),
-            BoolExpr::Next(sig) => BooleanSemantics::eval(sig, trace),
-            BoolExpr::Oracle(sig) => BooleanSemantics::eval(sig, trace),
-            BoolExpr::Always(sig) => BooleanSemantics::eval(sig, trace),
-            BoolExpr::Eventually(sig) => BooleanSemantics::eval(sig, trace),
-            BoolExpr::Until(sig) => BooleanSemantics::eval(sig, trace),
-        }
-    }
-}
+pub struct BooleanSemantics;
 
-impl BooleanSemantics for BoolLit {
-    fn eval(&self, _trace: &impl Trace) -> ArgusResult<Signal<bool>> {
-        Ok(Signal::constant(self.0))
-    }
-}
+impl BooleanSemantics {
+    pub fn eval(expr: &BoolExpr, trace: &impl Trace) -> ArgusResult<Signal<bool>> {
+        let ret = match expr {
+            BoolExpr::BoolLit(val) => Signal::constant(val.0),
+            BoolExpr::BoolVar(BoolVar { name }) => trace
+                .get::<bool>(name.as_str())
+                .ok_or(ArgusError::SignalNotPresent)?
+                .clone(),
+            BoolExpr::Cmp(Cmp { op, lhs, rhs }) => {
+                use argus_core::expr::Ordering::*;
+                let lhs = QuantitativeSemantics::eval_num_expr::<f64>(lhs, trace)?;
+                let rhs = QuantitativeSemantics::eval_num_expr::<f64>(rhs, trace)?;
 
-impl BooleanSemantics for BoolVar {
-    fn eval(&self, trace: &impl Trace) -> ArgusResult<Signal<bool>> {
-        trace
-            .get(self.name.as_str())
-            .cloned()
-            .ok_or(ArgusError::SignalNotPresent)
-    }
-}
-
-impl BooleanSemantics for Cmp {
-    fn eval(&self, trace: &impl Trace) -> ArgusResult<Signal<bool>> {
-        use argus_core::expr::Ordering::*;
-
-        let lhs = QuantitativeSemantics::eval(self.lhs.as_ref(), trace)?;
-        let rhs = QuantitativeSemantics::eval(self.rhs.as_ref(), trace)?;
-        let ret = match self.op {
-            Eq => lhs.signal_eq(&rhs),
-            NotEq => lhs.signal_ne(&rhs),
-            Less { strict } if *strict => lhs.signal_lt(&rhs),
-            Less { strict: _ } => lhs.signal_le(&rhs),
-            Greater { strict } if *strict => lhs.signal_gt(&rhs),
-            Greater { strict: _ } => lhs.signal_ge(&rhs),
+                match op {
+                    Eq => lhs.signal_eq(&rhs).unwrap(),
+                    NotEq => lhs.signal_ne(&rhs).unwrap(),
+                    Less { strict } if *strict => lhs.signal_lt(&rhs).unwrap(),
+                    Less { strict: _ } => lhs.signal_le(&rhs).unwrap(),
+                    Greater { strict } if *strict => lhs.signal_gt(&rhs).unwrap(),
+                    Greater { strict: _ } => lhs.signal_ge(&rhs).unwrap(),
+                }
+            }
+            BoolExpr::Not(Not { arg }) => {
+                let arg = Self::eval(arg, trace)?;
+                !&arg
+            }
+            BoolExpr::And(And { args }) => {
+                assert!(args.len() >= 2);
+                args.iter()
+                    .map(|arg| Self::eval(arg, trace))
+                    .try_fold(Signal::const_true(), |acc, item| {
+                        let item = item?;
+                        Ok(acc.and(&item))
+                    })?
+            }
+            BoolExpr::Or(Or { args }) => {
+                assert!(args.len() >= 2);
+                args.iter()
+                    .map(|arg| Self::eval(arg, trace))
+                    .try_fold(Signal::const_true(), |acc, item| {
+                        let item = item?;
+                        Ok(acc.or(&item))
+                    })?
+            }
+            BoolExpr::Next(Next { arg }) => {
+                let arg = Self::eval(arg, trace)?;
+                compute_next(arg)?
+            }
+            BoolExpr::Oracle(Oracle { steps, arg }) => {
+                let arg = Self::eval(arg, trace)?;
+                compute_oracle(arg, *steps)?
+            }
+            BoolExpr::Always(Always { arg, interval }) => {
+                let arg = Self::eval(arg, trace)?;
+                compute_always(arg, interval)?
+            }
+            BoolExpr::Eventually(Eventually { arg, interval }) => {
+                let arg = Self::eval(arg, trace)?;
+                compute_eventually(arg, interval)?
+            }
+            BoolExpr::Until(Until { lhs, rhs, interval }) => {
+                let lhs = Self::eval(lhs, trace)?;
+                let rhs = Self::eval(rhs, trace)?;
+                compute_until(lhs, rhs, interval)?
+            }
         };
-        ret.ok_or(ArgusError::InvalidOperation)
-    }
-}
-
-impl BooleanSemantics for Not {
-    fn eval(&self, trace: &impl Trace) -> ArgusResult<Signal<bool>> {
-        let arg = BooleanSemantics::eval(self.arg.as_ref(), trace)?;
-        Ok(arg.not())
-    }
-}
-
-impl BooleanSemantics for And {
-    fn eval(&self, trace: &impl Trace) -> ArgusResult<Signal<bool>> {
-        let mut ret = Signal::constant(true);
-        for arg in self.args.iter() {
-            let arg = Self::eval(arg, trace)?;
-            ret = ret.and(&arg);
-        }
-    }
-}
-
-impl BooleanSemantics for Or {
-    fn eval(&self, trace: &impl Trace) -> ArgusResult<Signal<bool>> {
-        let mut ret = Signal::constant(true);
-        for arg in self.args.iter() {
-            let arg = Self::eval(arg, trace)?;
-            ret = ret.or(&arg);
-        }
+        Ok(ret)
     }
 }
 
 fn compute_next(arg: Signal<bool>) -> ArgusResult<Signal<bool>> {
+    compute_oracle(arg, 1)
+}
+
+fn compute_oracle(arg: Signal<bool>, steps: usize) -> ArgusResult<Signal<bool>> {
+    if steps == 0 {
+        return Ok(Signal::Empty);
+    }
     match arg {
         Signal::Empty => Ok(Signal::Empty),
         sig @ Signal::Constant { value: _ } => {
@@ -96,37 +101,22 @@ fn compute_next(arg: Signal<bool>) -> ArgusResult<Signal<bool>> {
             mut time_points,
         } => {
             // TODO(anand): Verify this
-            // Just shift the signal by 1 timestamp
-            assert!(values.len() == time_points.len());
-            if values.len() <= 1 {
+            // Just shift the signal by `steps` timestamps
+            assert_eq!(values.len(), time_points.len());
+            if values.len() <= steps {
                 return Ok(Signal::Empty);
             }
-            values.remove(0);
-            time_points.pop();
+            let expected_len = values.len() - steps;
+            let values = values.split_off(steps);
+            let _ = time_points.split_off(steps);
+
+            assert_eq!(values.len(), expected_len);
+            assert_eq!(values.len(), time_points.len());
             Ok(Signal::Sampled { values, time_points })
         }
     }
 }
 
-impl BooleanSemantics for Next {
-    fn eval(&self, trace: &impl Trace) -> ArgusResult<Signal<bool>> {
-        let arg = BooleanSemantics::eval(self.arg.as_ref(), trace)?;
-        compute_next(arg)
-    }
-}
-
-impl BooleanSemantics for Oracle {
-    fn eval(&self, trace: &impl Trace) -> ArgusResult<Signal<bool>> {
-        if self.steps == 0 {
-            Ok(Signal::Empty)
-        } else {
-            (0..self.steps).try_fold(BooleanSemantics::eval(self.arg.as_ref(), trace)?, |arg, _| {
-                compute_next(arg)
-            })
-        }
-    }
-}
-
 /// Compute always for a signal
 fn compute_always(signal: Signal<bool>, interval: &Interval) -> ArgusResult<Signal<bool>> {
     if interval.is_empty() || interval.is_singleton() {
@@ -134,45 +124,20 @@ fn compute_always(signal: Signal<bool>, interval: &Interval) -> ArgusResult<Sign
             reason: "interval is either empty or singleton",
         });
     }
-    let ret = match signal {
-        // if signal is empty or constant, return the signal itself.
-        // This works because if a signal is True everythere, then it must
-        // "always be true".
-        sig @ (Signal::Empty | Signal::Constant { value: _ }) => sig,
-        sig => {
-            use Bound::*;
-            if interval.is_untimed() {
-                compute_untimed_always(sig)
-            } else if let (Included(a), Included(b)) = interval.into() {
-                compute_timed_always(sig, *a, Some(*b))
-            } else if let (Included(a), Unbounded) = interval.into() {
-                compute_timed_always(sig, *a, None)
-            } else {
-                unreachable!("interval should be created using Interval::new, and is_untimed checks this")
-            }
-        }
-    };
-    Ok(ret)
+    let z1 = !signal;
+    let z2 = compute_eventually(z1, interval)?;
+    Ok(!z2)
 }
 
 /// Compute timed always for the interval `[a, b]` (or, if `b` is `None`, `[a, ..]`.
-fn compute_timed_always(signal: Signal<bool>, a: Duration, b: Option<Duration>) -> Signal<bool> {
-    match b {
-        Some(b) => {
-            // We want to compute the windowed min/and of the signal.
-            // The window is dictated by the time duration though.
-            todo!()
-        }
-        None => {
-            // Shift the signal to the left by `a` and then run the untimed always.
-            let shifted = signal.shift_left(a);
-            compute_untimed_always(shifted)
-        }
-    }
+fn compute_timed_always(signal: Signal<bool>, a: Duration, b: Option<Duration>) -> ArgusResult<Signal<bool>> {
+    let z1 = !signal;
+    let z2 = compute_timed_eventually(z1, a, b)?;
+    Ok(!z2)
 }
 
 /// Compute untimed always
-fn compute_untimed_always(signal: Signal<bool>) -> Signal<bool> {
+fn compute_untimed_always(signal: Signal<bool>) -> ArgusResult<Signal<bool>> {
     let Signal::Sampled {
         mut values,
         time_points,
@@ -184,14 +149,7 @@ fn compute_untimed_always(signal: Signal<bool>) -> Signal<bool> {
     for i in (0..(time_points.len() - 1)).rev() {
         values[i] &= values[i + 1];
     }
-    Signal::Sampled { values, time_points }
-}
-
-impl BooleanSemantics for Always {
-    fn eval(&self, trace: &impl Trace) -> ArgusResult<Signal<bool>> {
-        let arg = BooleanSemantics::eval(&self.arg, trace)?;
-        compute_always(arg, &self.interval)
-    }
+    Ok(Signal::Sampled { values, time_points })
 }
 
 /// Compute eventually for a signal
@@ -212,11 +170,11 @@ fn compute_eventually(signal: Signal<bool>, interval: &Interval) -> ArgusResult<
                 // for singleton intervals, return the signal itself.
                 sig
             } else if interval.is_untimed() {
-                compute_untimed_eventually(sig)
+                compute_untimed_eventually(sig)?
             } else if let (Included(a), Included(b)) = interval.into() {
-                compute_timed_eventually(sig, *a, Some(*b))
+                compute_timed_eventually(sig, *a, Some(*b))?
             } else if let (Included(a), Unbounded) = interval.into() {
-                compute_timed_eventually(sig, *a, None)
+                compute_timed_eventually(sig, *a, None)?
             } else {
                 unreachable!("interval should be created using Interval::new, and is_untimed checks this")
             }
@@ -226,15 +184,42 @@ fn compute_eventually(signal: Signal<bool>, interval: &Interval) -> ArgusResult<
 }
 
 /// Compute timed eventually for the interval `[a, b]` (or, if `b` is `None`, `[a,..]`.
-fn compute_timed_eventually(signal: Signal<bool>, a: Duration, b: Option<Duration>) -> Signal<bool> {
+fn compute_timed_eventually(signal: Signal<bool>, a: Duration, b: Option<Duration>) -> ArgusResult<Signal<bool>> {
     match b {
         Some(b) => {
             // We want to compute the windowed max/or of the signal.
             // The window is dictated by the time duration though.
-            todo!()
+            let Signal::Sampled { values, time_points } = signal else {
+                unreachable!("we shouldn't be passing non-sampled signals here")
+            };
+            assert!(b > a);
+            assert!(!time_points.is_empty());
+            let signal_duration = *time_points.last().unwrap() - *time_points.first().unwrap();
+            let width = if signal_duration < (b - a) {
+                signal_duration
+            } else {
+                b - a
+            };
+            let mut ret_vals = Vec::with_capacity(values.len());
+
+            // For boolean signals we dont need to worry about intersections with ZERO as much as
+            // for quantitative signals, as linear interpolation is just a discrte switch.
+            let mut wedge = MonoWedge::<bool>::max_wedge(width);
+            for (i, value) in time_points.iter().zip(&values) {
+                wedge.update((i, value));
+                if i >= &(time_points[0] + width) {
+                    ret_vals.push(
+                        wedge
+                            .front()
+                            .map(|(&t, &v)| (t, v))
+                            .unwrap_or_else(|| panic!("wedge should have at least 1 element")),
+                    )
+                }
+            }
+            Signal::try_from_iter(ret_vals.into_iter())
         }
         None => {
-            // Shift the signal to the left by `a` and then run the untimedeventually.
+            // Shift the signal to the left by `a` and then run the untimed eventually.
             let shifted = signal.shift_left(a);
             compute_untimed_eventually(shifted)
         }
@@ -242,7 +227,7 @@ fn compute_timed_eventually(signal: Signal<bool>, a: Duration, b: Option<Duratio
 }
 
 /// Compute untimed eventually
-fn compute_untimed_eventually(signal: Signal<bool>) -> Signal<bool> {
+fn compute_untimed_eventually(signal: Signal<bool>) -> ArgusResult<Signal<bool>> {
     let Signal::Sampled {
         mut values,
         time_points,
@@ -254,14 +239,7 @@ fn compute_untimed_eventually(signal: Signal<bool>) -> Signal<bool> {
     for i in (0..(time_points.len() - 1)).rev() {
         values[i] |= values[i + 1];
     }
-    Signal::Sampled { values, time_points }
-}
-
-impl BooleanSemantics for Eventually {
-    fn eval(&self, trace: &impl Trace) -> ArgusResult<Signal<bool>> {
-        let arg = BooleanSemantics::eval(&self.arg, trace)?;
-        compute_eventually(arg, &self.interval)
-    }
+    Ok(Signal::Sampled { values, time_points })
 }
 
 /// Compute until
@@ -292,11 +270,11 @@ fn compute_until(lhs: Signal<bool>, rhs: Signal<bool>, interval: &Interval) -> A
         ) => {
             use Bound::*;
             if interval.is_untimed() {
-                compute_untimed_until(lhs, rhs)
+                compute_untimed_until(lhs, rhs)?
             } else if let (Included(a), Included(b)) = interval.into() {
-                compute_timed_until(lhs, rhs, *a, Some(*b))
+                compute_timed_until(lhs, rhs, *a, Some(*b))?
             } else if let (Included(a), Unbounded) = interval.into() {
-                compute_timed_until(lhs, rhs, *a, None)
+                compute_timed_until(lhs, rhs, *a, None)?
             } else {
                 unreachable!("interval should be created using Interval::new, and is_untimed checks this")
             }
@@ -306,31 +284,36 @@ fn compute_until(lhs: Signal<bool>, rhs: Signal<bool>, interval: &Interval) -> A
 }
 
 /// Compute timed until for the interval `[a, b]` (or, if `b` is `None`, `[a, ..]`.
-fn compute_timed_until(lhs: Signal<bool>, rhs: Signal<bool>, a: Duration, b: Option<Duration>) -> Signal<bool> {
-    // For this, we will perform the Until rewrite defined in [1]:
-    // $$
-    //  \varphi_1 U_{[a, b]} \varphi_2 = F_{[a,b]} \varphi_2 \land (\varphi_1 U_{[a,
-    // \infty)} \varphi_2)
-    // $$
-    //
-    // $$
-    //  \varphi_1 U_{[a, \infty)} \varphi_2 = G_{[0,a]} (\varphi_1 U \varphi_2)
-    // $$
-    //
-    // [1] A. Donzé, T. Ferrère, and O. Maler, "Efficient Robust Monitoring for STL."
-
+///
+/// For this, we will perform the Until rewrite defined in [1]:
+/// $$
+///  \varphi_1 U_{[a, b]} \varphi_2 = F_{[a,b]} \varphi_2 \land (\varphi_1 U_{[a,
+/// \infty)} \varphi_2)
+/// $$
+///
+/// $$
+///  \varphi_1 U_{[a, \infty)} \varphi_2 = G_{[0,a]} (\varphi_1 U \varphi_2)
+/// $$
+///
+/// [1]: <> (A. Donzé, T. Ferrère, and O. Maler, "Efficient Robust Monitoring for STL.")
+fn compute_timed_until(
+    lhs: Signal<bool>,
+    rhs: Signal<bool>,
+    a: Duration,
+    b: Option<Duration>,
+) -> ArgusResult<Signal<bool>> {
     match b {
         Some(b) => {
             // First compute eventually [a, b]
-            let ev_a_b_rhs = compute_timed_eventually(rhs, a, Some(b));
+            let ev_a_b_rhs = compute_timed_eventually(rhs.clone(), a, Some(b))?;
             // Then compute until [a, \infty) (lhs, rhs)
-            let unt_a_inf = compute_timed_until(lhs, rhs, a, None);
+            let unt_a_inf = compute_timed_until(lhs, rhs, a, None)?;
             // Then & them
-            &ev_a_b_rhs & &unt_a_inf
+            Ok(&ev_a_b_rhs & &unt_a_inf)
         }
         None => {
             // First compute untimed until (lhs, rhs)
-            let untimed_until = compute_untimed_until(lhs, rhs);
+            let untimed_until = compute_untimed_until(lhs, rhs)?;
             // Compute G [0, a]
             compute_untimed_always(untimed_until)
         }
@@ -338,13 +321,116 @@ fn compute_timed_until(lhs: Signal<bool>, rhs: Signal<bool>, a: Duration, b: Opt
 }
 
 /// Compute untimed until
-fn compute_untimed_until(lhs: Signal<bool>, rhs: Signal<bool>) -> Signal<bool> {
-    let sync_points = lhs.sync_with_intersection(&rhs);
+fn compute_untimed_until(lhs: Signal<bool>, rhs: Signal<bool>) -> ArgusResult<Signal<bool>> {
+    let sync_points = lhs.sync_with_intersection::<Linear>(&rhs);
     todo!()
 }
 
-impl BooleanSemantics for Until {
-    fn eval(&self, trace: &impl Trace) -> ArgusResult<Signal<bool>> {
-        todo!()
+#[cfg(test)]
+mod tests {
+    use std::collections::HashMap;
+
+    use argus_core::expr::ExprBuilder;
+    use argus_core::signals::AnySignal;
+    use itertools::assert_equal;
+
+    use super::*;
+
+    #[derive(Default)]
+    struct MyTrace {
+        signals: HashMap<String, Box<dyn AnySignal>>,
+    }
+
+    impl Trace for MyTrace {
+        fn signal_names(&self) -> Vec<&str> {
+            self.signals.keys().map(|key| key.as_str()).collect()
+        }
+
+        fn get<T: 'static>(&self, name: &str) -> Option<&Signal<T>> {
+            let signal = self.signals.get(name)?;
+            signal.as_any().downcast_ref::<Signal<T>>()
+        }
+    }
+
+    #[test]
+    fn less_than() {
+        let mut ctx = ExprBuilder::new();
+
+        let a = ctx.float_var("a".to_owned()).unwrap();
+        let spec = ctx.make_lt(a, ctx.float_const(0.0));
+
+        let signals = HashMap::from_iter(vec![(
+            "a".to_owned(),
+            Box::new(Signal::from_iter(vec![
+                (Duration::from_secs_f64(0.0), 1.3),
+                (Duration::from_secs_f64(0.7), 3.0),
+                (Duration::from_secs_f64(1.3), 0.1),
+                (Duration::from_secs_f64(2.1), -2.2),
+            ])) as Box<dyn AnySignal>,
+        )]);
+
+        let trace = MyTrace { signals };
+
+        let rob = BooleanSemantics::eval(&spec, &trace).unwrap();
+        let expected = Signal::from_iter(vec![
+            (Duration::from_secs_f64(0.0), false),
+            (Duration::from_secs_f64(0.7), false),
+            (Duration::from_secs_f64(1.3), false),
+            (Duration::from_secs_f64(1.334782609), true), // interpolated at
+            (Duration::from_secs_f64(2.1), true),
+        ]);
+
+        assert_equal(&rob, &expected);
+    }
+
+    #[test]
+    fn eventually_unbounded() {
+        let mut ctx = ExprBuilder::new();
+
+        let a = ctx.float_var("a".to_owned()).unwrap();
+        let cmp = ctx.make_ge(a, ctx.float_const(0.0));
+        let spec = ctx.make_eventually(cmp);
+
+        {
+            let signals = HashMap::from_iter(vec![(
+                "a".to_owned(),
+                Box::new(Signal::from_iter(vec![
+                    (Duration::from_secs_f64(0.0), 2.5),
+                    (Duration::from_secs_f64(0.7), 4.0),
+                    (Duration::from_secs_f64(1.3), -1.0),
+                    (Duration::from_secs_f64(2.1), 1.7),
+                ])) as Box<dyn AnySignal>,
+            )]);
+
+            let trace = MyTrace { signals };
+            let rob = BooleanSemantics::eval(&spec, &trace).unwrap();
+
+            let Signal::Sampled { values, time_points: _ } = rob else {
+                panic!("boolean semantics should remain sampled");
+            };
+            assert!(values.into_iter().all(|v| v));
+        }
+        {
+            let signals = HashMap::from_iter(vec![(
+                "a".to_owned(),
+                Box::new(Signal::from_iter(vec![
+                    (Duration::from_secs_f64(0.0), 2.5),
+                    (Duration::from_secs_f64(0.7), 4.0),
+                    (Duration::from_secs_f64(1.3), 1.7),
+                    (Duration::from_secs_f64(1.4), 0.0),
+                    (Duration::from_secs_f64(2.1), -2.0),
+                ])) as Box<dyn AnySignal>,
+            )]);
+
+            let trace = MyTrace { signals };
+            let rob = BooleanSemantics::eval(&spec, &trace).unwrap();
+            println!("{:#?}", rob);
+
+            let Signal::Sampled { values, time_points: _ } = rob else {
+                panic!("boolean semantics should remain sampled");
+            };
+            assert!(values[..values.len() - 1].iter().all(|&v| v));
+            assert!(!values[values.len() - 1]);
+        }
     }
 }
diff --git a/argus-semantics/src/semantics/mod.rs b/argus-semantics/src/semantics/mod.rs
index 6f96a7c..7f76a75 100644
--- a/argus-semantics/src/semantics/mod.rs
+++ b/argus-semantics/src/semantics/mod.rs
@@ -1,2 +1,5 @@
-pub mod boolean;
-// pub mod quantitative;
+mod boolean;
+mod quantitative;
+
+pub use boolean::BooleanSemantics;
+pub use quantitative::QuantitativeSemantics;
diff --git a/argus-semantics/src/semantics/quantitative.rs b/argus-semantics/src/semantics/quantitative.rs
index 54f991b..166f4e5 100644
--- a/argus-semantics/src/semantics/quantitative.rs
+++ b/argus-semantics/src/semantics/quantitative.rs
@@ -1,41 +1,29 @@
-use std::iter::zip;
+use std::ops::Bound;
+use std::time::Duration;
 
-use argus_core::expr::{Always, And, BoolExpr, BoolVar, Cmp, Eventually, Next, Not, Or, Oracle, Until};
+use argus_core::expr::*;
 use argus_core::prelude::*;
-use argus_core::signals::traits::{SignalAbs, SignalMinMax};
-use argus_core::signals::SignalNumCast;
+use argus_core::signals::interpolation::Linear;
+use argus_core::signals::SignalAbs;
+use num_traits::{Num, NumCast};
 
-use crate::eval::eval_num_expr;
-use crate::Trace;
+use crate::traits::Trace;
+use crate::utils::lemire_minmax::MonoWedge;
 
-fn top_or_bot(sig: &Signal<bool>) -> Signal<f64> {
-    match sig {
-        Signal::Empty => Signal::Empty,
-        Signal::Constant { value } => Signal::constant(*value).to_f64().unwrap(),
-        Signal::Sampled { values, time_points } => zip(time_points, values)
-            .map(|(&t, &v)| if v { (t, f64::INFINITY) } else { (t, f64::NEG_INFINITY) })
-            .collect(),
-    }
-}
-
-/// Quantitative semantics for Argus expressions
 pub struct QuantitativeSemantics;
 
-impl Semantics for QuantitativeSemantics {
-    type Output = Signal<f64>;
-    type Context = ();
-
-    fn eval(expr: &BoolExpr, trace: &impl Trace, ctx: Self::Context) -> ArgusResult<Self::Output> {
-        let ret: Self::Output = match expr {
+impl QuantitativeSemantics {
+    pub fn eval(expr: &BoolExpr, trace: &impl Trace) -> ArgusResult<Signal<f64>> {
+        let ret = match expr {
             BoolExpr::BoolLit(val) => top_or_bot(&Signal::constant(val.0)),
-            BoolExpr::BoolVar(BoolVar { name }) => {
-                let sig = trace.get::<bool>(name.as_str()).ok_or(ArgusError::SignalNotPresent)?;
-                top_or_bot(sig)
-            }
+            BoolExpr::BoolVar(BoolVar { name }) => trace
+                .get::<bool>(name.as_str())
+                .ok_or(ArgusError::SignalNotPresent)
+                .map(top_or_bot)?,
             BoolExpr::Cmp(Cmp { op, lhs, rhs }) => {
                 use argus_core::expr::Ordering::*;
-                let lhs = eval_num_expr::<f64>(lhs, trace)?;
-                let rhs = eval_num_expr::<f64>(rhs, trace)?;
+                let lhs = Self::eval_num_expr::<f64>(lhs, trace)?;
+                let rhs = Self::eval_num_expr::<f64>(rhs, trace)?;
 
                 match op {
                     Eq => -&((&lhs - &rhs).abs()),
@@ -45,69 +33,584 @@ impl Semantics for QuantitativeSemantics {
                 }
             }
             BoolExpr::Not(Not { arg }) => {
-                let arg = Self::eval(arg, trace, ctx)?;
+                let arg = Self::eval(arg, trace)?;
                 -&arg
             }
             BoolExpr::And(And { args }) => {
                 assert!(args.len() >= 2);
-                let args = args
-                    .iter()
-                    .map(|arg| Self::eval(arg, trace, ctx))
-                    .collect::<ArgusResult<Vec<_>>>()?;
-                args.into_iter()
-                    .reduce(|lhs, rhs| lhs.min(&rhs))
-                    .ok_or(ArgusError::InvalidOperation)?
+                args.iter().map(|arg| Self::eval(arg, trace)).try_fold(
+                    Signal::constant(f64::INFINITY),
+                    |acc, item| {
+                        let item = item?;
+                        Ok(acc.min(&item))
+                    },
+                )?
             }
             BoolExpr::Or(Or { args }) => {
                 assert!(args.len() >= 2);
-                let args = args
-                    .iter()
-                    .map(|arg| Self::eval(arg, trace, ctx))
-                    .collect::<ArgusResult<Vec<_>>>()?;
-                args.into_iter()
-                    .reduce(|lhs, rhs| lhs.max(&rhs))
-                    .ok_or(ArgusError::InvalidOperation)?
+                args.iter().map(|arg| Self::eval(arg, trace)).try_fold(
+                    Signal::constant(f64::NEG_INFINITY),
+                    |acc, item| {
+                        let item = item?;
+                        Ok(acc.max(&item))
+                    },
+                )?
             }
-            BoolExpr::Next(Next { arg: _ }) => todo!(),
-            BoolExpr::Oracle(Oracle { steps: _, arg: _ }) => todo!(),
-            BoolExpr::Always(Always { arg, interval: _ }) => {
-                let mut arg = Self::eval(arg, trace, ctx)?;
-                match &mut arg {
-                    // if signal is empty or constant, return the signal itself.
-                    // This works because if a signal is positive everywhere, then it must
-                    // "always be positive" (and vice versa).
-                    Signal::Empty | Signal::Constant { value: _ } => (),
-                    Signal::Sampled { values, time_points } => {
-                        // Compute the min in a expanding window fashion from the back
-                        for i in (0..(time_points.len() - 1)).rev() {
-                            values[i] = values[i].min(values[i + 1]);
-                        }
-                    }
-                }
-                arg
+            BoolExpr::Next(Next { arg }) => {
+                let arg = Self::eval(arg, trace)?;
+                compute_next(arg)?
             }
-            BoolExpr::Eventually(Eventually { arg, interval: _ }) => {
-                let mut arg = Self::eval(arg, trace, ctx)?;
-                match &mut arg {
-                    // if signal is empty or constant, return the signal itself.
-                    // This works because if a signal is positive somewhere, then it must
-                    // "eventually be positive" (and vice versa).
-                    Signal::Empty | Signal::Constant { value: _ } => (),
-                    Signal::Sampled { values, time_points } => {
-                        // Compute the max in a expanding window fashion from the back
-                        for i in (0..(time_points.len() - 1)).rev() {
-                            values[i] = values[i].max(values[i + 1]);
-                        }
-                    }
-                }
-                arg
+            BoolExpr::Oracle(Oracle { steps, arg }) => {
+                let arg = Self::eval(arg, trace)?;
+                compute_oracle(arg, *steps)?
+            }
+            BoolExpr::Always(Always { arg, interval }) => {
+                let arg = Self::eval(arg, trace)?;
+                compute_always(arg, interval)?
+            }
+            BoolExpr::Eventually(Eventually { arg, interval }) => {
+                let arg = Self::eval(arg, trace)?;
+                compute_eventually(arg, interval)?
+            }
+            BoolExpr::Until(Until { lhs, rhs, interval }) => {
+                let lhs = Self::eval(lhs, trace)?;
+                let rhs = Self::eval(rhs, trace)?;
+                compute_until(lhs, rhs, interval)?
             }
-            BoolExpr::Until(Until {
-                lhs: _,
-                rhs: _,
-                interval: _,
-            }) => todo!(),
         };
         Ok(ret)
     }
+
+    pub fn eval_num_expr<T>(root: &NumExpr, trace: &impl Trace) -> ArgusResult<Signal<T>>
+    where
+        T: Num + NumCast,
+        for<'a> &'a Signal<T>: std::ops::Neg<Output = Signal<T>>,
+        for<'a> &'a Signal<T>: std::ops::Add<&'a Signal<T>, Output = Signal<T>>,
+        for<'a> &'a Signal<T>: std::ops::Sub<&'a Signal<T>, Output = Signal<T>>,
+        for<'a> &'a Signal<T>: std::ops::Mul<&'a Signal<T>, Output = Signal<T>>,
+        for<'a> &'a Signal<T>: std::ops::Div<&'a Signal<T>, Output = Signal<T>>,
+        Signal<T>: SignalAbs,
+    {
+        match root {
+            NumExpr::IntLit(val) => Signal::constant(val.0).num_cast(),
+            NumExpr::UIntLit(val) => Signal::constant(val.0).num_cast(),
+            NumExpr::FloatLit(val) => Signal::constant(val.0).num_cast(),
+            NumExpr::IntVar(IntVar { name }) => trace.get::<i64>(name.as_str()).unwrap().num_cast(),
+            NumExpr::UIntVar(UIntVar { name }) => trace.get::<u64>(name.as_str()).unwrap().num_cast(),
+            NumExpr::FloatVar(FloatVar { name }) => trace.get::<f64>(name.as_str()).unwrap().num_cast(),
+            NumExpr::Neg(Neg { arg }) => Self::eval_num_expr::<T>(arg, trace).map(|sig| -&sig),
+            NumExpr::Add(Add { args }) => {
+                let mut ret: Signal<T> = Signal::<T>::zero();
+                for arg in args.iter() {
+                    let arg = Self::eval_num_expr::<T>(arg, trace)?;
+                    ret = &ret + &arg;
+                }
+                Ok(ret)
+            }
+            NumExpr::Sub(Sub { lhs, rhs }) => {
+                let lhs = Self::eval_num_expr::<T>(lhs, trace)?;
+                let rhs = Self::eval_num_expr::<T>(rhs, trace)?;
+                Ok(&lhs - &rhs)
+            }
+            NumExpr::Mul(Mul { args }) => {
+                let mut ret: Signal<T> = Signal::<T>::one();
+                for arg in args.iter() {
+                    let arg = Self::eval_num_expr::<T>(arg, trace)?;
+                    ret = &ret * &arg;
+                }
+                Ok(ret)
+            }
+            NumExpr::Div(Div { dividend, divisor }) => {
+                let dividend = Self::eval_num_expr::<T>(dividend, trace)?;
+                let divisor = Self::eval_num_expr::<T>(divisor, trace)?;
+                Ok(&dividend / &divisor)
+            }
+            NumExpr::Abs(Abs { arg }) => {
+                let arg = Self::eval_num_expr::<T>(arg, trace)?;
+                Ok(arg.abs())
+            }
+        }
+    }
+}
+
+fn compute_next(arg: Signal<f64>) -> ArgusResult<Signal<f64>> {
+    compute_oracle(arg, 1)
+}
+
+fn compute_oracle(arg: Signal<f64>, steps: usize) -> ArgusResult<Signal<f64>> {
+    if steps == 0 {
+        return Ok(Signal::Empty);
+    }
+    match arg {
+        Signal::Empty => Ok(Signal::Empty),
+        sig @ Signal::Constant { value: _ } => {
+            // Just return the signal as is
+            Ok(sig)
+        }
+        Signal::Sampled {
+            mut values,
+            mut time_points,
+        } => {
+            // TODO(anand): Verify this
+            // Just shift the signal by `steps` timestamps
+            assert_eq!(values.len(), time_points.len());
+            if values.len() <= steps {
+                return Ok(Signal::Empty);
+            }
+            let expected_len = values.len() - steps;
+            let values = values.split_off(steps);
+            let _ = time_points.split_off(steps);
+
+            assert_eq!(values.len(), expected_len);
+            assert_eq!(values.len(), time_points.len());
+            Ok(Signal::Sampled { values, time_points })
+        }
+    }
+}
+
+/// Compute always for a signal
+fn compute_always(signal: Signal<f64>, interval: &Interval) -> ArgusResult<Signal<f64>> {
+    if interval.is_empty() || interval.is_singleton() {
+        return Err(ArgusError::InvalidInterval {
+            reason: "interval is either empty or singleton",
+        });
+    }
+    let ret = match signal {
+        // if signal is empty or constant, return the signal itself.
+        // This works because if a signal is True everythere, then it must
+        // "always be true".
+        sig @ (Signal::Empty | Signal::Constant { value: _ }) => sig,
+        sig => {
+            use Bound::*;
+            if interval.is_singleton() {
+                // for singleton intervals, return the signal itself.
+                sig
+            } else if interval.is_untimed() {
+                compute_untimed_always(sig)?
+            } else if let (Included(a), Included(b)) = interval.into() {
+                compute_timed_always(sig, *a, Some(*b))?
+            } else if let (Included(a), Unbounded) = interval.into() {
+                compute_timed_always(sig, *a, None)?
+            } else {
+                unreachable!("interval should be created using Interval::new, and is_untimed checks this")
+            }
+        }
+    };
+    Ok(ret)
+}
+
+/// Compute timed always for the interval `[a, b]` (or, if `b` is `None`, `[a, ..]`.
+fn compute_timed_always(signal: Signal<f64>, a: Duration, b: Option<Duration>) -> ArgusResult<Signal<f64>> {
+    let z1 = -signal;
+    let z2 = compute_timed_eventually(z1, a, b)?;
+    Ok(-z2)
+}
+
+/// Compute untimed always
+fn compute_untimed_always(signal: Signal<f64>) -> ArgusResult<Signal<f64>> {
+    let Signal::Sampled {
+        mut values,
+        time_points,
+    } = signal
+    else {
+        unreachable!("we shouldn't be passing non-sampled signals here")
+    };
+    // Compute the & in a expanding window fashion from the back
+    for i in (0..(time_points.len() - 1)).rev() {
+        values[i] = values[i + 1].min(values[i]);
+    }
+    Ok(Signal::Sampled { values, time_points })
+}
+
+/// Compute eventually for a signal
+fn compute_eventually(signal: Signal<f64>, interval: &Interval) -> ArgusResult<Signal<f64>> {
+    if interval.is_empty() || interval.is_singleton() {
+        return Err(ArgusError::InvalidInterval {
+            reason: "interval is either empty or singleton",
+        });
+    }
+    let ret = match signal {
+        // if signal is empty or constant, return the signal itself.
+        // This works because if a signal is True everythere, then it must
+        // "eventually be true".
+        sig @ (Signal::Empty | Signal::Constant { value: _ }) => sig,
+        sig => {
+            use Bound::*;
+            if interval.is_singleton() {
+                // for singleton intervals, return the signal itself.
+                sig
+            } else if interval.is_untimed() {
+                compute_untimed_eventually(sig)?
+            } else if let (Included(a), Included(b)) = interval.into() {
+                compute_timed_eventually(sig, *a, Some(*b))?
+            } else if let (Included(a), Unbounded) = interval.into() {
+                compute_timed_eventually(sig, *a, None)?
+            } else {
+                unreachable!("interval should be created using Interval::new, and is_untimed checks this")
+            }
+        }
+    };
+    Ok(ret)
+}
+
+/// Compute timed eventually for the interval `[a, b]` (or, if `b` is `None`, `[a,..]`.
+fn compute_timed_eventually(signal: Signal<f64>, a: Duration, b: Option<Duration>) -> ArgusResult<Signal<f64>> {
+    match b {
+        Some(b) => {
+            // We want to compute the windowed max/or of the signal.
+            // The window is dictated by the time duration though.
+            let Signal::Sampled { values, time_points } = signal else {
+                unreachable!("we shouldn't be passing non-sampled signals here")
+            };
+            assert!(b > a);
+            assert!(!time_points.is_empty());
+            let signal_duration = *time_points.last().unwrap() - *time_points.first().unwrap();
+            let width = if signal_duration < (b - a) {
+                signal_duration
+            } else {
+                b - a
+            };
+            let mut ret_vals = Vec::with_capacity(values.len());
+
+            // For boolean signals we dont need to worry about intersections with ZERO as much as
+            // for quantitative signals, as linear interpolation is just a discrte switch.
+            let mut wedge = MonoWedge::<f64>::max_wedge(width);
+            for (i, value) in time_points.iter().zip(&values) {
+                wedge.update((i, value));
+                if i >= &(time_points[0] + width) {
+                    ret_vals.push(
+                        wedge
+                            .front()
+                            .map(|(&t, &v)| (t, v))
+                            .unwrap_or_else(|| panic!("wedge should have at least 1 element")),
+                    )
+                }
+            }
+            Signal::try_from_iter(ret_vals.into_iter())
+        }
+        None => {
+            // Shift the signal to the left by `a` and then run the untimed eventually.
+            let shifted = signal.shift_left(a);
+            compute_untimed_eventually(shifted)
+        }
+    }
+}
+
+/// Compute untimed eventually
+fn compute_untimed_eventually(signal: Signal<f64>) -> ArgusResult<Signal<f64>> {
+    let Signal::Sampled {
+        mut values,
+        time_points,
+    } = signal
+    else {
+        unreachable!("we shouldn't be passing non-sampled signals here")
+    };
+    // Compute the | in a expanding window fashion from the back
+    for i in (0..(time_points.len() - 1)).rev() {
+        values[i] = values[i + 1].max(values[i]);
+    }
+    Ok(Signal::Sampled { values, time_points })
+}
+
+/// Compute until
+fn compute_until(lhs: Signal<f64>, rhs: Signal<f64>, interval: &Interval) -> ArgusResult<Signal<f64>> {
+    let ret = match (lhs, rhs) {
+        // If either signals are empty, return empty
+        (sig @ Signal::Empty, _) | (_, sig @ Signal::Empty) => sig,
+        (lhs, rhs) => {
+            use Bound::*;
+            if interval.is_untimed() {
+                compute_untimed_until(lhs, rhs)?
+            } else if let (Included(a), Included(b)) = interval.into() {
+                compute_timed_until(lhs, rhs, *a, Some(*b))?
+            } else if let (Included(a), Unbounded) = interval.into() {
+                compute_timed_until(lhs, rhs, *a, None)?
+            } else {
+                unreachable!("interval should be created using Interval::new, and is_untimed checks this")
+            }
+        }
+    };
+    Ok(ret)
+}
+
+/// Compute timed until for the interval `[a, b]` (or, if `b` is `None`, `[a, ..]`.
+///
+/// For this, we will perform the Until rewrite defined in [1]:
+/// $$
+///  \varphi_1 U_{[a, b]} \varphi_2 = F_{[a,b]} \varphi_2 \land (\varphi_1 U_{[a,
+/// \infty)} \varphi_2)
+/// $$
+///
+/// $$
+///  \varphi_1 U_{[a, \infty)} \varphi_2 = G_{[0,a]} (\varphi_1 U \varphi_2)
+/// $$
+///
+/// [1]: <> (A. Donzé, T. Ferrère, and O. Maler, "Efficient Robust Monitoring for STL.")
+fn compute_timed_until(
+    lhs: Signal<f64>,
+    rhs: Signal<f64>,
+    a: Duration,
+    b: Option<Duration>,
+) -> ArgusResult<Signal<f64>> {
+    match b {
+        Some(b) => {
+            // First compute eventually [a, b]
+            let ev_a_b_rhs = compute_timed_eventually(rhs.clone(), a, Some(b))?;
+            // Then compute until [a, \infty) (lhs, rhs)
+            let unt_a_inf = compute_timed_until(lhs, rhs, a, None)?;
+            // Then & them
+            Ok(ev_a_b_rhs.min(&unt_a_inf))
+        }
+        None => {
+            assert_ne!(a, Duration::ZERO, "untimed case wasn't handled for Until");
+            // First compute untimed until (lhs, rhs)
+            let untimed_until = compute_untimed_until(lhs, rhs)?;
+            // Compute G [0, a]
+            compute_timed_always(untimed_until, Duration::ZERO, Some(a))
+        }
+    }
+}
+
+/// Compute untimed until
+fn compute_untimed_until(lhs: Signal<f64>, rhs: Signal<f64>) -> ArgusResult<Signal<f64>> {
+    let sync_points = lhs.sync_with_intersection::<Linear>(&rhs).unwrap();
+    let mut ret_samples = Vec::with_capacity(sync_points.len());
+    let expected_len = sync_points.len();
+
+    let mut next = f64::NEG_INFINITY;
+
+    for (i, t) in sync_points.into_iter().enumerate().rev() {
+        let v1 = lhs.interpolate_at::<Linear>(t).unwrap();
+        let v2 = rhs.interpolate_at::<Linear>(t).unwrap();
+
+        let z = f64::max(f64::min(v1, v2), f64::min(v1, next));
+        if z == next && i < (expected_len - 2) {
+            ret_samples.pop();
+        }
+        ret_samples.push((t, z));
+        next = z;
+    }
+
+    Signal::<f64>::try_from_iter(ret_samples.into_iter().rev())
+}
+
+fn top_or_bot(sig: &Signal<bool>) -> Signal<f64> {
+    let bool2float = |&v| {
+        if v {
+            f64::INFINITY
+        } else {
+            f64::NEG_INFINITY
+        }
+    };
+    match sig {
+        Signal::Empty => Signal::Empty,
+        Signal::Constant { value } => Signal::constant(bool2float(value)),
+        Signal::Sampled { values, time_points } => {
+            time_points.iter().copied().zip(values.iter().map(bool2float)).collect()
+        }
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use std::collections::HashMap;
+    use std::iter::zip;
+    use std::time::Duration;
+
+    use argus_core::expr::ExprBuilder;
+    use argus_core::signals::AnySignal;
+    use itertools::assert_equal;
+
+    use super::*;
+
+    const FLOAT_EPS: f64 = 1.0e-8;
+
+    fn assert_approx_eq(lhs: &Signal<f64>, rhs: &Signal<f64>) {
+        zip(lhs, rhs).enumerate().for_each(|(i, (s1, s2))| {
+            assert_eq!(
+                s1.0, s2.0,
+                "Failed assertion {:?} != {:?} for iteration {}",
+                s1.0, s2.0, i
+            );
+            assert!(
+                (s2.1 - s1.1).abs() <= FLOAT_EPS,
+                "Failed approx equal assertion: {} != {} for iteration {}",
+                s1.1,
+                s2.1,
+                i
+            );
+        });
+    }
+
+    #[derive(Default)]
+    struct MyTrace {
+        signals: HashMap<String, Box<dyn AnySignal>>,
+    }
+
+    impl Trace for MyTrace {
+        fn signal_names(&self) -> Vec<&str> {
+            self.signals.keys().map(|key| key.as_str()).collect()
+        }
+
+        fn get<T: 'static>(&self, name: &str) -> Option<&Signal<T>> {
+            let signal = self.signals.get(name)?;
+            signal.as_any().downcast_ref::<Signal<T>>()
+        }
+    }
+
+    #[test]
+    fn num_constant() {
+        let expr_builder = ExprBuilder::new();
+
+        let spec = expr_builder.float_const(5.0);
+        let trace = MyTrace::default();
+
+        let robustness = QuantitativeSemantics::eval_num_expr::<f64>(&spec, &trace).unwrap();
+
+        assert!(matches!(robustness, Signal::Constant { value } if value == 5.0));
+    }
+
+    #[test]
+    fn addition() {
+        let mut ctx = ExprBuilder::new();
+
+        let a = ctx.float_var("a".to_owned()).unwrap();
+        let b = ctx.float_var("b".to_owned()).unwrap();
+        let spec = ctx.make_add([*a, *b]).unwrap();
+
+        {
+            let signals = HashMap::from_iter(vec![
+                (
+                    "a".to_owned(),
+                    Box::new(Signal::from_iter(vec![
+                        (Duration::from_secs_f64(0.0), 1.3),
+                        (Duration::from_secs_f64(0.7), 3.0),
+                        (Duration::from_secs_f64(1.3), 0.1),
+                        (Duration::from_secs_f64(2.1), -2.2),
+                    ])) as Box<dyn AnySignal>,
+                ),
+                (
+                    "b".to_owned(),
+                    Box::new(Signal::from_iter(vec![
+                        (Duration::from_secs_f64(0.0), 2.5),
+                        (Duration::from_secs_f64(0.7), 4.0),
+                        (Duration::from_secs_f64(1.3), -1.2),
+                        (Duration::from_secs_f64(2.1), 1.7),
+                    ])) as Box<dyn AnySignal>,
+                ),
+            ]);
+
+            let trace = MyTrace { signals };
+
+            let rob = QuantitativeSemantics::eval_num_expr::<f64>(&spec, &trace).unwrap();
+            let expected = Signal::from_iter(vec![
+                (Duration::from_secs_f64(0.0), 1.3 + 2.5),
+                (Duration::from_secs_f64(0.7), 3.0 + 4.0),
+                (Duration::from_secs_f64(1.3), 0.1 + -1.2),
+                (Duration::from_secs_f64(2.1), -2.2 + 1.7),
+            ]);
+
+            assert_equal(&rob, &expected);
+        }
+        {
+            let signals = HashMap::from_iter(vec![
+                (
+                    "a".to_owned(),
+                    Box::new(Signal::from_iter(vec![
+                        (Duration::from_secs_f64(0.0), 1.3),
+                        (Duration::from_secs_f64(0.7), 3.0),
+                        (Duration::from_secs_f64(1.3), 4.0),
+                        (Duration::from_secs_f64(2.1), 3.0),
+                    ])) as Box<dyn AnySignal>,
+                ),
+                (
+                    "b".to_owned(),
+                    Box::new(Signal::from_iter(vec![
+                        (Duration::from_secs_f64(0.0), 2.5),
+                        (Duration::from_secs_f64(0.7), 4.0),
+                        (Duration::from_secs_f64(1.3), 3.0),
+                        (Duration::from_secs_f64(2.1), 4.0),
+                    ])) as Box<dyn AnySignal>,
+                ),
+            ]);
+
+            let trace = MyTrace { signals };
+
+            let rob = QuantitativeSemantics::eval_num_expr::<f64>(&spec, &trace).unwrap();
+            let expected = Signal::from_iter(vec![
+                (Duration::from_secs_f64(0.0), 1.3 + 2.5),
+                (Duration::from_secs_f64(0.7), 3.0 + 4.0),
+                (Duration::from_secs_f64(1.3), 4.0 + 3.0),
+                (Duration::from_secs_f64(2.1), 3.0 + 4.0),
+            ]);
+
+            assert_equal(&rob, &expected);
+        }
+    }
+
+    #[test]
+    fn less_than() {
+        let mut ctx = ExprBuilder::new();
+
+        let a = ctx.float_var("a".to_owned()).unwrap();
+        let spec = ctx.make_lt(a, ctx.float_const(0.0));
+
+        let signals = HashMap::from_iter(vec![(
+            "a".to_owned(),
+            Box::new(Signal::from_iter(vec![
+                (Duration::from_secs_f64(0.0), 1.3),
+                (Duration::from_secs_f64(0.7), 3.0),
+                (Duration::from_secs_f64(1.3), 0.1),
+                (Duration::from_secs_f64(2.1), -2.2),
+            ])) as Box<dyn AnySignal>,
+        )]);
+
+        let trace = MyTrace { signals };
+
+        let rob = dbg!(QuantitativeSemantics::eval(&spec, &trace).unwrap());
+        let expected = Signal::from_iter(vec![
+            (Duration::from_secs_f64(0.0), 0.0 - 1.3),
+            (Duration::from_secs_f64(0.7), 0.0 - 3.0),
+            (Duration::from_secs_f64(1.3), 0.0 - 0.1),
+            (Duration::from_secs_f64(1.334782609), 0.0), // interpolated at
+            (Duration::from_secs_f64(2.1), 0.0 - (-2.2)),
+        ]);
+
+        assert_approx_eq(&rob, &expected);
+    }
+
+    #[test]
+    fn eventually_unbounded() {
+        let mut ctx = ExprBuilder::new();
+
+        let a = ctx.float_var("a".to_owned()).unwrap();
+        let cmp = ctx.make_ge(a, ctx.float_const(0.0));
+        let spec = ctx.make_eventually(cmp);
+
+        {
+            let signals = HashMap::from_iter(vec![(
+                "a".to_owned(),
+                Box::new(Signal::from_iter(vec![
+                    (Duration::from_secs_f64(0.0), 2.5),
+                    (Duration::from_secs_f64(0.7), 4.0),
+                    (Duration::from_secs_f64(1.3), -1.0),
+                    (Duration::from_secs_f64(2.1), 1.7),
+                ])) as Box<dyn AnySignal>,
+            )]);
+
+            let trace = MyTrace { signals };
+            let rob = QuantitativeSemantics::eval(&spec, &trace).unwrap();
+            println!("{:#?}", rob);
+            let expected = Signal::from_iter(vec![
+                (Duration::from_secs_f64(0.0), 4.0),
+                (Duration::from_secs_f64(0.7), 4.0),
+                (Duration::from_secs_f64(1.18), 1.7),
+                (Duration::from_secs_f64(1.3), 1.7),
+                (Duration::from_secs_f64(1.596296296), 1.7), // interpolated at
+                (Duration::from_secs_f64(2.1), 1.7),
+            ]);
+
+            assert_equal(&rob, &expected);
+        }
+    }
 }
diff --git a/argus-semantics/src/traits.rs b/argus-semantics/src/traits.rs
index fda3b3a..e5f96d3 100644
--- a/argus-semantics/src/traits.rs
+++ b/argus-semantics/src/traits.rs
@@ -1,6 +1,5 @@
 //! Traits to define semantics for temporal logic specifications
 
-use argus_core::expr::{IsBoolExpr, IsNumExpr};
 use argus_core::prelude::*;
 
 /// A trace is a collection of signals
@@ -50,13 +49,3 @@ pub trait Trace {
     /// Query a signal using its name
     fn get<T: 'static>(&self, name: &str) -> Option<&Signal<T>>;
 }
-
-/// Boolean semantics for a [`BoolExpr`] or type that is
-/// convertable to a [`BoolExpr`]
-pub trait BooleanSemantics: IsBoolExpr {
-    fn eval(&self, trace: &impl Trace) -> ArgusResult<Signal<bool>>;
-}
-
-pub trait QuantitativeSemantics: IsNumExpr {
-    fn eval(&self, trace: &impl Trace) -> ArgusResult<Signal<bool>>;
-}
diff --git a/argus-semantics/src/utils/lemire_minmax.rs b/argus-semantics/src/utils/lemire_minmax.rs
index 5e00962..6439656 100644
--- a/argus-semantics/src/utils/lemire_minmax.rs
+++ b/argus-semantics/src/utils/lemire_minmax.rs
@@ -8,6 +8,8 @@
 //! [^2]: Daniel Lemire. 2007. Streaming Maximum-Minimum Filter Using No More than Three
 //! Comparisons per Element. arXiv:cs/0610046.
 
+// TODO: Make a MonoWedge iterator adapter.
+
 use std::collections::VecDeque;
 use std::time::Duration;