A modern, dependently
typed Lisp

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.

The Haskell phase has been about reworking Serene's foundations around type theory. The highlights: a new REPL and a rewrite of the semantic analysis, a growing body of dependent-type research, and the first piece of Serene's universe hierarchy — the Universe type.

This is the groundwork for moving Serene to a dependently typed core, and it sets the direction for everything that follows.