Author(s)
Presentation
Un même matériel informatique peut remplir de nombreuses fonctions différentes par simple changement du logiciel qu’il exécute. Cette extraordinaire plasticité a permis à l’ordinateur de sortir des centres de calcul et de se répandre partout, des objets du quotidien aux infrastructures de la cité. Quels concepts fondamentaux sous-tendent cette prouesse technique ? Comment maîtriser l'incroyable et souvent effrayante complexité du logiciel ? Comment éviter les « bugs » de programmation et résister aux attaques ? Comment établir qu’un logiciel est digne de confiance ? À ces questions, la logique mathématique offre des éléments de réponse qui permettent de construire une approche scientifiquement rigoureuse du logiciel.
Ce livre est la réédition par le Collège de France de l’ouvrage publié sous le même titre en 2019 (Collège de France/Fayard).
Xavier Leroy est informaticien, spécialiste des langages et outils de programmation. Il est l’un des auteurs du langage OCaml et du compilateur formellement vérifié CompCert. Précédemment chercheur à l’Inria, il a été nommé professeur au Collège de France, titulaire de la chaire Sciences du logiciel, en mai 2018.
Table of contents
Une brève histoire du logiciel
Les fondations logiques
Vers l'efficacité: algorithmique et programmation
Les langages de la programmation
Le typage
La vérification formelle
Conclusion
Same author
All publications from the same author
Dominique Charpin, Xavier Leroy
Déchiffrement(s) : des hiéroglyphes à l’ADN
Xavier Leroy
Le logiciel, entre l’esprit et la matière
Same collection
All publications from the same collection
Pascale Senellart-Mardon
Atomes artificiels et photons au cœur d'une seconde révolution quantique
Thierry Coquand
La théorie des types, de Russell aux assistants à la démonstration
Franck Courchamp
Les paradoxes de la biodiversité
Yanick Lahens
Haitian Literature: Urgency(ies) of Writing, Dream(s) of Inhabiting