Ioana Pasca

Starting from December 2010 I am a post-doc at LIP in Lyon. Look for my new webpage on the Arénaire team page.

Previously 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.

For more details on my PhD, look at this page.

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