Certification de programmes avec des effets calculatoires

Keywords :

• état
• exceptions
• preuves de programmes
• sémantique equationnelle
• logique décorée
• certification de programmes
• Coq

In this thesis, we aim to formalize the effects of a computation. Indeed, most used programming languages involve different sorts of effects: state change, exceptions, input/output, non-determinism, etc. They may bring ease and flexibility to the coding process. However, the problem is to take into account the effects when proving the properties of programs. The major difficulty in such kind of reasoning is the mismatch between the syntax of operations with effects and their interpretation.

Typically, a piece of program with arguments in X that returns a value in Y is not interpreted as a function from X to Y, due to the effects. The best-known algebraic approach to the problem interprets programs including effects with the use of monads: the interpretation is a function from X to T(Y) where T is a monad. This approach has been extended to Lawvere theories and algebraic handlers. Another approach called, the decorated logic, provides a sort of equational semantics for reasoning about programs with effects. We specialize the approach of decorated logic to the state and the exceptions effects by defining the decorated logic for states (L_st) and the decorated logic for exceptions (L_exc), respectively. This enables us to prove properties of programs involving such effects. Then, we formalize these logics in Coq and certify the related proofs. These logics are built so as to be sound. In addition, we introduce a relative notion of syntactic completeness of a theory in a given logic with respect to a sublogic. We prove that the decorated theory for the global states as well as two decorated theories for exceptions are syntactically complete relatively to their pure sublogics. These proofs are certified in Coq as applications of our generic frameworks.

Directors:

• Mr Jean Guillaume Dumas (Professeur - Université Joseph Fourier )
• Mme Dominique Duval (Professeure - Université Joseph Fourier )

Raporteurs:

• Mme Catherine Dubois (Professeur - ENSIIE )
• Mr Olivier Laurent (Directeur de Recherche - CNRS )
• Mr Alan Schmitt (Directeur de Recherche - INRIA )

Examinators:

• Mr Andrej Bauer (Professeur - Université de Ljubljana )
• Mr Jean François Monin (Professeur - Université Joseph Fourier )
• Mr Damien Pous (Chercheur - CNRS )