A modern, dependently
typed Lisp

I've just wrapped up a three-part series on my personal blog about how concurrency works inside Serene's runtime - from picking the core abstraction all the way to a working HTTP server built on it.

If you've ever wondered why Serene uses fibers, how they can suspend across JIT and foreign C frames without function colouring, or how the scheduler and IO reactor fit together, this is the deep dive:

1. Part 1 — Choosing the Building Blocks A tour of the popular concurrency building blocks — threads, callbacks, async/await — what each one costs, and why fibers won.

2. Part 2 — Fibers, the Scheduler and the Reactor Inside Serene's fibers: frozen call chains, guard pages, a scheduler that knows nothing, and the IO Reactor that feeds it.

3. Part 3 — A Tiny HTTP Server Putting the fibers and IO Reactor to work in a small HTTP server that spawns a fiber per connection.

Best read in order, but each part stands on its own. Feedback welcome!

Serene's runtime is now can be used as a generic, standalone library; and can be utilized in any program. It licensed under the GNU LGPL v3.

It also splits cleanly. Build it with -Dwith-serene=disabled and you get just the generic substrate that does not include any Serene specific APIs.

So the pieces that were always general-purpose are now usable on their own. Pull in libserene.runtime through pkg-config and you're all set.

For more info check the runtime guide out.

The runtime now has an M:N, work-stealing fiber scheduler: stackful, cooperative fibers multiplexed across OS-thread workers, each with its own local run queue and work stealing between them. See the runtime API and the language report for details.

lscz2's pipeline is now organised around a graph. Namespaces are the graph's nodes, terms are added to it as they are checked, and evaluated values are fed back into the graph as values.

This end-to-end loop — Syntax → Expr (Semantic) → core terms → values — replaces the old linear pass structure and better matches how a dependently typed program is actually elaborated.

The stage-0 compiler has been ported from Haskell (lscz) to Idris2 (lscz2). With a dependently typed host language we can express Serene's type theory directly rather than encoding it.

This phase brought an elaborator from the high-level surface language down to the corett core, a bidirectional type checker for Kernel.TT, and the Parser and compiler Pipeline ported over to Idris2. Serene is now being built on Quantitative Type Theory — see the language report.

Serene now has a dedicated C runtime, and over the second half of 2025 it took shape. It gained persistent CHAMP/HAMT data structures and an event loop via libuv, and — replacing an earlier Boehm GC experiment — a custom, block-based memory manager (mm).

Along the way: tagged-union values, an atomic object-id counter, and gensym. See the runtime API reference for the details.