Ioana Pasca

Starting from September 2011 I am an ATER (temporary teaching assistant) at ENS de Lyon in the Arénaire team. Previously I was a post-doc in the same team, in the ANR project TaMaDi .

Before this, I was a PhD student in the Marelle team at INRIA Sophia Antipolis where I worked under the supervision of Yves Bertot on formalization of real and numerical analysis concepts in the Coq proof system.

I was also part of the Mathematical Components project of the Microsoft Research - INRIA joint center. I use the SSReflect extension of the Coq system as well as the libraries developed upon it in the project.

Key words for my research interests: formal verification, proof assistants, type theory, formalization of mathematical theories, verification of computations and numerical methods.