Le 23 avril 2012, à 14h en salle B311, le séminaire LCR accueille Paolo Parisen Toldin (Bologne).

Contrary to ICC standard approach, we present a small WHILE language characterizing the class PP.

The main problem concerning the imperative approach is to understand how informations/values flow throw variables in a program.

In literature are well known many works that have polytime soundness but just few of them (using the imperative paradigm) are able to give a polytime completeness.

Our system, MAL0 (Multiplied, Affine, Linear, 0 dependeces ), is sound and complete. Moreover, our system can be used also to check if a program is running in probabilistic polytime (can be easily restrict to just polytime soundness). We claim that, contrary to works found in literature, our system is able to certify a program in polytime.

This is a joint work in progress with Jean-Yves Moyen.