Home > Researchers > Ioana Pasca

Researchers

Back to the list

A A

Ioana Pasca

Former member

Microsoft Research-Inria (PHD Student)

Mathematical Components

Presentation

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.

Contact:

[email protected]

+330000000

Personal web page

Publications at the Joint Centre:

2013

Conference papers

titre: A Machine-Checked Proof of the Odd Order Theorem
auteur: Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O’Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, Laurent Théry
article: Sandrine Blazy and Christine Paulin and David Pichardie. ITP 2013, 4th Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. Springer, 7998, pp.163-179, 2013, LNCS. <10.1007/978-3-642-39634-2_14>
Accès au texte intégral et bibtex

2008

Conference papers

titre: Canonical Big Operators
auteur: Yves Bertot, Georges Gonthier, Sidi Ould Biha, Ioana Pasca
article: Theorem Proving in Higher Order Logics, Aug 2008, Montreal, Canada. 5170/2008, 2008, LNCS. <10.1007/978-3-540-71067-7>
Accès au texte intégral et bibtex