Le LAMA entretient quatre séminaires réguliers, qui se tiennent normalement dans la salle TLR, premier étage du bâtiment Le Chablais, sur le site du Bourget du Lac. D’une part, trois séminaires hebdomadaires existent :
- Séminaire de l’équipe EDPs2.
- Séminaire de l’équipe de géométrie, habituellement le vendredi à 10h.
- Séminaire de l’équipe de logique, habituellement le jeudi à 10h15 et commun avec l'équipe Plume (ENS Lyon).
D’autre part, le séminaire du laboratoire a lieu environ tous les trois mois. Il reçoit une personnalité extérieure de renom, sur des sujets pouvant intéresser des membres de plusieurs équipes, ou bien un nouveau membre du laboratoire.
Enfin, le séminaire des doctorants a lieu tous les deux mois environ et accueille un jeune chercheur (doctorant, post-doc ou ATER), du Lama ou de la région, pour une présentation d'une heure accessible à tous.
Prochains séminaires :
EDPs2Vendredi 31 mai 2013 à 14h, Seignosse Le Penon, Landes
GéométrieVendredi 14 juin 2013 à 10h15
Résumé : (Masquer les résumés)
À venir
LIMDJeudi 23 mai 2013 à 10h
Résumé : (Masquer les résumés)
Dependant Linear PCF (dlPCF) was introduced by Dal Lago and Gaboardi as a type system characterising the complexity of PCF programs. It is parametrised by a an equational program, which is used to express some complexity annotations for types. This enables a modular complexity analysis, and the main strength of the system is to be relatively complete: any terminating PCF program is typable in dlPCF (and its complexity is thus determined) assuming that the equational program is expressive enough. We have designed a type inference algorithm for this system: given a PCF program, it computes its type in dlPCF (and thus a complexity bound for the program) together with a set of proof obligations that ensures the correctness of the type, following the same scenario as the computation of weakest preconditions in Hoare logic. Checking formally the proof obligations generated by the type checker then amounts to a formal proof that the complexity bound is correct. In this talk I will explain how the type system dlPCF can be turned into a tool for formal certification of the complexity of functional programs.