Accéder au contenu.
Menu Sympa

athena - [ATHENA] Séminaire Codes Sources : Démonstrations assistées par ordinateur (Assia Mahboubi, 7 février 2019)

athena AT services.cnrs.fr

Objet : Histoire des techniques

Archives de la liste

[ATHENA] Séminaire Codes Sources : Démonstrations assistées par ordinateur (Assia Mahboubi, 7 février 2019)


Chronologique Discussions 
  • From: Baptiste Mélès <baptiste.meles AT gmail.com>
  • To: educasup.philo AT ml.free.fr, theuth AT listes.univ-rennes1.fr, athena AT services.cnrs.fr, emetis AT listes.univ-paris1.fr, codes-sources AT googlegroups.com, diff AT pps.univ-paris-diderot.fr
  • Subject: [ATHENA] Séminaire Codes Sources : Démonstrations assistées par ordinateur (Assia Mahboubi, 7 février 2019)
  • Date: Fri, 25 Jan 2019 11:32:45 +0100
  • Authentication-results: t2gpsmtp1.dsi.cnrs.fr (amavisd-new); dkim=pass (2048-bit key) header.d=gmail.com

Séminaire « Codes sources »

L'objectif du séminaire Codes sources est de présenter la pensée
informatique là où elle s'exprime le plus concrètement : dans les textes
que sont les codes sources.


Séance du jeudi 7 février 2019 (14h-16h) :

Assia Mahboubi (Inria, LS2N, Université de Nantes) :

« Démonstrations assistées par ordinateur »


Résumé :

Les ordinateurs ont profondément transformé la pratique des
mathématiques contemporaines, mettant en particulier leur puissance de
calcul au service de l'observation, de la conjecture et même de la
validation "par calcul". La généralisation rapide de l'accès à une
puissance de calcul surhumaine a même suscité de nouvelles formes de
mathématiques, à l'interface avec l'informatique, comme le calcul
formel ou l'analyse numérique. Moins connus que certains systèmes de
calcul symbolique, numérique ou statistique, les "assistants de
preuve" font néanmoins partie des logiciels qui permettent de faire
des mathématiques sur ordinateur. Ils sont conçus pour aider leurs
utilisateurs à représenter définitions, énoncés et démonstrations dans
un formalisme logique précis et non ambigu, sous la forme de
bibliothèques digitales de mathématiques formalisées. Il existe
plusieurs sous-familles d'assistants de preuves, qui diffèrent en
particulier sur le choix de fondations logiques, qui détermine le
langage formel utilisé. En particulier, une majorité d'entre eux sont
basés sur une forme de théorie des types, une approche des fondations
logiques qui donne une place privilégiée aux fonctions, et au concept
de calcul. Mais dans tous les case, une telle (ré)écriture des
théories mathématiques serait bien trop piétonne pour être
envisageable, sinon intéressante, sans l'aide de la machine. Cette
dernière permet en retour de réduire la vérification des preuves à une
tâche routinière et mécanisée. Mais ce n'est pas le seul bénéfice
d'une telle formalisation et nous discuterons dans cet exposé la
pratique et les enjeux de cette forme de mathématiques assistées par
ordinateur.

Cet exposé ne présuppose pas de connaissance particulière en logique
ou en programmation.


Lieu :

Salle 24-25/405 du LIP6 (rotonde 25, 4e étage)


Adresse :

4 place Jussieu, 75005 Paris
métro Jussieu (lignes 7 et 10)


------------------------------------------------------------------------

Prochaines séances du séminaire Codes sources :

- Jeudi 28 mars 2019 : Bastien GUERRY, « Code source et/ou
documentation ? Réflexions autour de l’éditeur Emacs, du langage Emacs
Lisp et du module Org-mode »

- Jeudi 11 avril 2019 : Marie-José DURAND-RICHARD (Paris 8, SPHERE),
« Les diagrammes de fonctionnement de The Analytical Engine, de
Charles Babbage 1791-1877) à Ada Lovelace (1815-1852) »

- Jeudi 23 mai 2019 : à déterminer

- Jeudi 13 juin 2019 : à déterminer

Sauf mention contraire, toutes les séances ont lieu de 14 heures à
16 heures au LIP6.



------------------------------------------------------------------------

/* ***************************************
* À propos du séminaire Codes sources *
*************************************** */

À celui seul qui prend la peine de les lire effectivement, les codes
sources révèlent leur richesse. On y découvre que l'élégance d'un
algorithme réside parfois hors de sa complexité, dans l'usage virtuose
des idiomes du langage de programmation ou dans la connaissance fine de
la machine à laquelle il est destiné. Bien souvent des codes sources
comportent davantage de lignes de commentaires que de code. Tous ces
trésors de pensée informatique fondent à la compilation comme neige au
soleil — preuve qu'un programme n'est pas seulement écrit pour être
compilé.

Le but du séminaire est de décrire ces œuvres de l'esprit comme des
textes à part entière. Nous espérons ainsi contribuer à la constitution
d'une culture générale en programmation. En informatique comme en
littérature, cela suppose la familiarisation progressive avec un corpus
de grands textes.

À chaque séance, un intervenant — jeune chercheur ou chercheur confirmé
en informatique, en histoire ou en philosophie — présente, en moins
d'une heure, un code source de son choix : un fragment de système
d'exploitation, de pilote, de compilateur, de bibliothèque... Le code
peut avoir été écrit par l'orateur ou par quelqu'un d'autre, dans
quelque langage que ce soit. Le commentaire peut être algorithmique,
stylistique, historique ou philosophique, et porter sur tous les aspects
du code, commentaires compris. Le code est ensuite discuté avec
l'auditoire.


Organisateurs :

- Raphaël Fournier (CNAM)
- Baptiste Mélès (CNRS, Archives Henri-Poincaré)
- Lionel Tabourier (LIP6).

Site : http://codesource.hypotheses.org/

Contact : Baptiste Mélès (baptiste.meles AT univ-lorraine.fr)

Twitter : https://twitter.com/SemCodesSources

Liste de diffusion : https://groups.google.com/forum/#!forum/codes-sources

------------------------------------------------------------------------


--
Baptiste Mélès
Chargé de recherche au CNRS (CNRS Researcher)
Archives Henri-Poincaré—Philosophie et Recherches sur les Sciences et
les Technologies (CNRS UMR 7117, http://poincare.univ-lorraine.fr)
Université de Lorraine — Université de Strasbourg
/Philosophia Scientiæ/ (Rédacteur en chef adjoint / Managing editor)
https://journals.openedition.org/philosophiascientiae/
91 avenue de la Libération, 54000 Nancy, France
http://baptiste.meles.free.fr/


  • [ATHENA] Séminaire Codes Sources : Démonstrations assistées par ordinateur (Assia Mahboubi, 7 février 2019), Baptiste Mélès, 25/01/2019

Archives gérées par MHonArc 2.6.18.

Haut de le page