In this talk, I will present the monitoring calculus, which is the result of a new forcing program transformation. It's a lambda calculus with a state that is able to monitor the execution of programs (this "monitoring" being a parameter of the machine). This mechanism is similar to what happens in Miquel's KFAM (Krivine Forcing Abstract Machine).

Based on this calculus, I define the notion of Forcing Computational Algebra (FCA), which internalizes the composition of linear forcing with a more usual biorthogonality-based realizability. As we will see, by considering different FCAs, we obtain realizability frameworks for various programming languages (for example featuring higher-order references, recursive types, bounded-time/space execution, streams, etc.), all sharing a common soundness result.

I will also show how the well-known technique of iterated forcing corresponds in our framework to a certain construction on FCAs, allowing us to combine different programming features in a modular way.

The ultimate goal of this work is to obtain a general, modular, algebraic framework in which we design and combine realizability models for all kind of programming languages.