Auteur(s)
Présentation
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.
Sommaire
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
Du même auteur
Toutes les publications du même auteur
Dominique Charpin, Xavier Leroy
Déchiffrement(s) : des hiéroglyphes à l’ADN
Xavier Leroy
Le logiciel, entre l’esprit et la matière
Dans la même collection
Toutes les publications dans la 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