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 (Lst) and the decorated logic for exceptions (Lexc),
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.
Keywords: computational effects, states, exceptions, program property proofs, equational
semantics, decorated logic, proof certification, Coq. |