Séance de 15 juin

Lieu: STL, Université de Lille 3, Salle Corbin (Bât. B, salle B1 661)

Nous avons le plaisir de vous annoncer la prochaîne et dernière séance du séminaire « Réflexions sur les processus de calcul, d’information et de programmation”, mercredi 15 juin 2016 à 14h, UMR 8163 STL, Université de Lille 3, Salle D. Corbin (Bât. B, salle B1 661) avec la participation de Gerard Chazal et Dale Miller.

Gerard Chazal (Université de Bourgogne), Informatique et philosophie du langage

Dans la mesure où un dispositif informatique fonctionne à partir de systèmes de codage, de langages artificiels assurant la communication entre l’homme et la machine, de syntaxes plus ou moins rigoureuses, deux rencontres devenaient inévitables :

1) celle de l’informatique et de la linguistique.

2) celle de l’informatique et de la philosophie du langage.

La première de ces rencontres a eu lieu très tôt, dès les débuts de l’informatique et de là, cette dernière a pu apparaître comme une manière d’aborder certains problèmes de philosophie du langage.

Après avoir présenté quelques problèmes de philosophie du langage susceptibles d’être éclairés par les pratiques de l’informatique, et après avoir examiné les rapports entre informatique et linguistique, nous montrerons plus précisément à travers deux approches techniques du langage quelques conséquences philosophiques.

Dale Miller (Inria and LIX/Ecole polytechnique),  Applications of structural proof theory to computer science

The field of computational logic encompasses many topics, including model checking, automatic and interactive theorem proving, type inference and static analysis, functional and logic programming, and the specification of and reasoning about computational systems.  Whichformal framework or frameworks can provide a foundation for thesevarious topics: should it be type theory, game theory, model theory, category theory, etc?  Some of these frameworks have been used to establish deep and important results: for example, Gödel’s model theoretic approach to completeness and the game theoretic approach tosequentiality for PCF.  These frameworks, however, do not seem appropriate for providing the initial chapters of a textbook introduction to these various topics.  I will argue in this talk thatthe topic of proof theory—dating back to Gentzen’s original sequent calculus and refined by Girard’s linear logic—provides a suitable such framework, especially one employs the focused versions of sequentcalculi.  I will survey recent work on getting proof theory to providea meaningful foundation for many of these topics in computational logic.