|
|||||
|
Defended on January 16th, 2014. Reviewers: Gilles Barthe (IMDEA, Spain), Lars Birkedal (Aarhus University, Denmark), Hans Boehm (HP Labs, USA). Jury members: Gilles Barthe (IMDEA, Spain), Lars Birkedal (Aarhus University, Denmark), Giuseppe Castagna (CNRS, France), Andrew Kennedy (Microsoft Research, UK), Xavier Leroy (INRIA, France), Xavier Rival (CNRS, France), André Seznec (INRIA, France).
The amazing complexity of today's programming calls for a new
engineering approach to build robust systems. Recent progress in
formal methods and mechanised proof assistants have made it possible
to apply mathematically rigorous methods to the specification, testing
and verification of ambitious projects. Nevertheless, despite some
remarkable successes, working with full-scale, realistic, system
interfaces is still in its infancy and novel tools and reasoning
techniques are needed to support a major change in the engineering
practice.
In this spirit, each chapter of my mémoire d'habilitation
proposes a solution to a problem arising from programming experience:
Chapter 1 points out how shared memory is a subtle model of
computation, and shows how to rigorously build sound abstractions of
the relaxed memory exhibited by mainstream programming languages and
architectures;
Chapter 2 illustrates how hard concurrency problems, as hunting
concurrency compiler bugs, can be made tractable via semantic
techniques that enable thread-wise reasoning;
Chapter 3 discusses the difficulties of formalising language
definitions, introduces the Ott tool for the working semanticist and
reports on five years of user feedback;
Chapter 4 explores the design space to integrate typed and
untyped code in scripting languages and presents a sweet spot where
programmers benefit from the best of the two worlds.
Each chapter ends with some open research directions that constitute
necessary and significant steps towards making modern systems easier
to program, analyse and test.
Other resources:
Acknowledgments (in italian).
|