Reasoning between Programming Languages and Architectures

Francesco Zappa Nardelli 1
1 Parkas - Parallélisme de Kahn Synchrone
DI-ENS - Département d'informatique de l'École normale supérieure, ENS Paris - École normale supérieure - Paris, Inria Paris-Rocquencourt, CNRS - Centre National de la Recherche Scientifique : UMR 8548
Abstract : 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 this 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, in my opinion, constitute necessary and significant steps towards making modern systems easier to program, analyse and test.
Type de document :
HDR
Computer Science [cs]. ENS Paris - Ecole Normale Supérieure de Paris, 2014
Liste complète des métadonnées


https://hal.inria.fr/tel-01110117
Contributeur : Francesco Zappa Nardelli <>
Soumis le : mardi 27 janvier 2015 - 15:27:23
Dernière modification le : jeudi 29 septembre 2016 - 01:22:39
Document(s) archivé(s) le : mardi 28 avril 2015 - 11:00:22

Fichier

Identifiants

  • HAL Id : tel-01110117, version 1

Collections

Citation

Francesco Zappa Nardelli. Reasoning between Programming Languages and Architectures. Computer Science [cs]. ENS Paris - Ecole Normale Supérieure de Paris, 2014. <tel-01110117>

Partager

Métriques

Consultations de
la notice

320

Téléchargements du document

104