The monitoring power of forcing program transformations
Aloïs Brunel · HAL (Le Centre pour la Communication Scientifique Directe) · 2014
In this thesis, we are interested in semantical proofs of correctness results for complex programming languages. In particular, we advocate the need for a theoretical framework that allows one to:- design realizability semantics using basic blocks - use algebraic constructions to combine those blocks As a step towards this goal, we propose a new semantical framework, based on the composition of linear variants of Krivine realizability and Cohen forcing. The first ingredient of this framework is the Monitoring Abstract Machine: a computing environment that possesses special memory cells used to monitor the execution of programs, in the style of Miquel's KFAM. It is shown how this new machine emerges from a linear forcing program transformation. We then introduce the central notion of Monitoring Algebra and the associated realizability interpretation. Different monitoring algebras induce sound semantics of different programming languages. We then present an algebraic construction to combine different Monitoring Algebras (and the associated programming languages) based on the technique of forcing iteration. We present various results and first applications of our theory. We show that the forcing structure can be used to represent the consumption of resources, in particular time, but also step-indexing or the use of higher-order references. We finally apply our results to retrieve three complex soundness results:- we give the first semantical proof of the consistency of a contraction-free naive set theory, originally introduced by Grishin- we use our framework to obtain a polynomial time termination result for a light-logic based programming language featuring recursive types - we prove the soundness of a language with references that supports strong updates, based on a linear type system inspired by a work of Ahmed, Fluet and Morrisett.