Français Anglais
Accueil Annuaire Plan du site
Home > Research results > Dissertations & habilitations
Research results
Ph.D de

Ph.D
Group : Toccata

Formalisation et développement d'une tactique réflexive pour la démonstration automatique en Coq

Starts on 16/07/2007
Advisor : CONTEJEAN, Evelyne

Funding : CDD sur contrat INRIA
Affiliation : Université Paris-Sud
Laboratory : LRI-INRIA PROVAL

Defended on 04/01/2011, committee :
Rapporteurs
Pierre Crégut (Orange Labs)
Shankar Natarajan (SRI)

Examinateurs
Hugo Herbelin (INRIA)
Sava Krstic (Intel)
Burkhart Wolff (Paris-Sud)

Encadrants
Evelyne Contejean (CNRS)
Sylvain Conchon (Paris-Sud)

Research activities :

Abstract :
n this thesis, we propose new automation capabilities for the Coq
proof assistant. We obtain this mechanization via an integration into
Coq of decision procedures for propositional logic, equality reasoning
and linear arithmetic which make up the core of the Alt-Ergo SMT
solver. This integration is achieved through the reflection technique,
which consists in implementing and formally proving these algorithms
in Coq in order to execute them directly in the proof
assistant. Because the algorithms formalized in Coq are exactly those
in use in Alt-Ergo's kernel, this work significantly increases our
trust in the solver. In particular, it embeds an original algorithm
for combining equality modulo theory reasoning, called CC(X) and
inspired by the Shostak combination algorithm, and whose justification
is quite complex.

Our Coq implementation is available in the form of tactics which allow
one to automatically solve formulae combining propositional logic,
equality and arithmetic. In order to make these tactics as efficient
as may be, we have taken special care with performance in our
implementation, in particular through the use of classical efficient
data structures, which we provide as a separate library.

Ph.D. dissertations & Faculty habilitations
APPRENTISSAGE ET OPTIMISATION SUR LES GRAPHES


ANALYSE DE DONNéES MULTI-MODALES POUR LES PATHOLOGIES COMPLEXES PAR LA CONCEPTION ET L’IMPLéMENTATION DE PROTOCOLES REPRODUCTIBLES ET RéUTILISABLES


DESIGNING INTERACTIVE TOOLS FOR CREATORS AND CREATIVE WORK
Creative work has been at the core of research in Human-Computer Interaction (HCI). I describe the results of a series of studies that look at how creators work, where creators include artists with years of professional practice, as well as learners, or novices and casual makers. My research focuses on three creation activities: drawing, physical modeling, and music composition. For these activities, I examine how artists switch between representations and how these representations evolve throughout their creative process, from early sketches to fine-grained forms or structured vocabularies. I present interactive systems that enrich their workflow (i) by extending their computer tools with physical user interfaces, or (ii) by making physical materials interactive. I also argue that sketch-based representations can allow for user interfaces that are more personal and less rigid. My presentation will reflect on lessons and limitations of this work and discuss challenges for future design-support tools.