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
DECODING THE PLATFORM SOCIETY: ORGANIZATIONS, MARKETS AND NETWORKS IN THE DIGITAL ECONOMY
The original manuscript conceptualizes the recent rise of digital platforms along three main dimensions: their nature of coordination devices fueled by data, the ensuing transformations of labor, and the accompanying promises of societal innovation. The overall ambition is to unpack the coordination role of the platform and where it stands in the horizon of the classical firm – market duality. It is also to precisely understand how it uses data to do so, where it drives labor, and how it accommodates socially innovative projects. I extend this analysis to show continuity between today’s society dominated by platforms and the “organizational society”, claiming that platforms are organized structures that distribute resources, produce asymmetries of wealth and power, and push social innovation to the periphery of the system. I discuss the policy implications of these tendencies and propose avenues for follow-up research.

DISTRIBUTED COMPUTING WITH LIMITED RESOURCES


VALORISATION DES DONNéES POUR LA RECHERCHE D'EMPLO