Studies

I made my master 2 internship at the LIX and the ISEP under supervision of Olivier Hermant and Gilles Dowek. I did some work about quantitative reducibility candidates, a framework to study light logics proofnets complexity properties. This work was based on Krivine's classical realizability and Hofmann & Dal Lago realizability.

Here is the report I wrote:

I made my second year internship at the RIMS (Kyoto, Japan), under supervision of Kazushige Terui.

I studied realizability techniques for implicit complexity. In particular, I established a new characterization of the complexity class FP (the polynomial time computable functions) as the functions representable by lambda-terms typable in DIAL (a dual system derived from affine linear logic) by the formula

                    Church => Scott  

where Church represents the type of Church integers, and Scott is the type of Scott integers (a purely linear representation of integers). To prove this result, I used a realizability model derived from the one introduced by Dal Lago and Hofmann in http://arxiv.org/pdf/cs/0506079.

Here is the paper presenting the results obtained during this internship:

Under supervision of Alexandre Miquel (PPS, Paris), I formalized in Coq the Krivine's classical realizability.