Categorical Semantics and Verification of Reactive Programs

This PhD project will aim for a categorical semantics and program logics of reactive programs. Categorical structures are well-suited as semantics of programs with generic effects: they allow precise tailoring of the axioms to specific classes of programs, and provide the necessary abstraction and compositionality that ease human understanding.

Reactive programs take infinite streams of inputs and produce infinite streams of outputs [1]. Such programs express models or specifications of machines that run indefinitely: machines that receive inputs from the environment and produce outputs accordingly. The outputs of these machines are not assumed to depend functionally on the inputs, so that programs may express probabilistic models, such as partially observable Markov decision processes [6], or allow other kinds of program effects, such as nondeterminism and access to a global state.

Pos...