Reasoning between Programming Languages and Architectures
Dossier scientifique pour l'obtention de l'habilitation à diriger les recherches
Francesco Zappa Nardelli

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

  • Reasoning between Programming Languages and Architectures, Francesco Zappa Nardelli, mémoire d'habilitation, 2013. [.pdf].

  • Slides, January 16th, 2014. [.pdf].

    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:

  • a recent CV [.pdf];
  • all my publications are available here;
  • most of the software I developed is available here.

    Acknowledgments (in italian).

  • Last update: