Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, EpiSciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
Skip to Main content Skip to Navigation
Habilitation à diriger des recherches

Reasoning between Programming Languages and Architectures

Francesco Zappa Nardelli 1 
1 Parkas - Parallélisme de Kahn Synchrone
DI-ENS - Département d'informatique - ENS 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.
Document type :
Habilitation à diriger des recherches
Complete list of metadata

Cited literature [89 references]  Display  Hide  Download
Contributor : Francesco Zappa Nardelli Connect in order to contact the contributor
Submitted on : Tuesday, January 27, 2015 - 3:27:23 PM
Last modification on : Thursday, March 17, 2022 - 10:08:44 AM
Long-term archiving on: : Tuesday, April 28, 2015 - 11:00:22 AM



  • HAL Id : tel-01110117, version 1



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



Record views


Files downloads