Dates

propositions: 24 septembre
inscription: 4 octobre
journées: 12-14 octobre

Contact

stephan.merz@loria.fr

Journées Nationales GEOCAL-LAC-LTP 2015

LORIA, Nancy, 12 – 14 octobre 2015

Les groupes de travail GeoCal (Géométrie du calcul) et LAC (Logique, Algèbre et Calcul) du GDR IM (Informatique Mathématique), ainsi que LTP (Langages, Types et Preuves) du GDR GPL (Génie de la Programmation et du Logiciel) organisent leur réunion annuelle 2015 en commun au LORIA du 12 au 14 octobre 2015.

La problématique du groupe de travail GeoCal (Géométrie du calcul) est de trouver au sein de la logique et des mathématiques des outils permettant la modélisation abstraite des programmes. Dans ce cadre général les travaux concernent la correspondance entre preuves et programmes (sémantiques de réalisabilité, extension de systèmes de types, calculs parallèles, ...), la complexité implicite visant à représenter des classes de complexité algorithmique par des contraintes logiques, le cadre topologique pour la concurrence et la géométrie de la réécriture, l'exploration de pistes pour unifier les paradigmes de calcul séquentiel et parallèle et d'autres thèmes similaires.

Le groupe de travail LAC (Logique, Algèbre et Calcul) fédère des chercheurs français travaillant sur les interactions entre les systèmes calculatoires issus de l'algèbre, comme les systèmes de réécriture de premier ordre ou les automates d'arbres, et ceux dont la base provient plutôt d'un système logique comme le lambda-calcul ou les réseaux de preuve ou interaction sans oublier les formalismes informatiques issus de la théorie des catégories. Le but des travaux est d'une part, d'exploiter le transfert de techniques entre ces formalismes, et d'autre part, d'étudier la possibilité de faire coexister ces approches dans un cadre homogène intégrant plusieurs paradigmes.

Les travaux du groupe de travail LTP (Langages, Types et Preuves) s'intéressent à la conception de langages plus sûrs et plus expressifs, au développement de techniques de vérification et de validation à partir de spécifications ou de code, à la vérification des outils de développement et à la vérification d'algorithmes. Ainsi, le groupe étudie des systèmes de types et de preuves et leur application à une programmation sûre, par exemple à travers la vérification ou l'inférence des types de manière statique ou dynamique. Le volet preuve du groupe concerne le développement de techniques et outils pour la preuve mais aussi l'utilisation de ces outils dans le cadre du développement de logiciels de confiance.

Exposés invités

Les chercheurs suivants ont accepté notre invitation à présenter leurs travaux lors de ces journées :

Participation aux journées

Il est demandé aux personnes intéressées de proposer des exposés, au plus tard pour le 24 septembre 2015.

Les inscriptions aux journées sont ouvertes jusqu'au 4 octobre 2015. La participation est gratuite, grâce aux soutiens généreux des GDR et du LORIA.