Events

Archives

Share:
A A
3 June 2009
Inauguration de la chaire “Microsoft-CNRS Optimisation et développement durable” (OSD) de l’Ecole Polytechnique
09:30-10:00 Accueil  10:00-12:20 Inauguration  10:00-10:30 Allocution d’accueil du Général de division Xavier Michel, Directeur général de l’École Polytechnique, intervention d’Éric Boustouller, Président de Microsoft France et de Pierre Guillon, Directeur de l’Institut ST2I du CNRS  10 :30-10:50 Communication de Madame Nathalie Kosciusko-Morizet Secrétaire d’État chargée de la ... More
3 June 2009
Rick Rashid visits the Joint Centre
Rick Rashid, Senior Vice President at Microsoft, Head of Microsoft Research, visits the Joint Centre on June 3, 2009, afternoon. We will have short talks and demos. Temptative program is:   13:00-14:00: Lunch 14:30-14:50 Introduction: JJL (1st floor, conference room) 15:00-17:30 Demos: 15:00-15:20, Mathematical Components Laurent Théry (1st floor, conference room) 15:20-15:40, Secure distributed ... More
6 May 2009
Bruno Salvy fait un exposé sur les Preuves automatiques d’identités
Orsay, Bat I, 1er étage, Centre de Recherche commun INRIA-MSR Preuves automatiques d’identités Bruno Salvy, INRIA Depuis une vingtaine d’années, le calcul formel a beaucoup progressé dans l’algorithmisation des mathématiques. En particulier, quelques idées simples mais fécondes permettent maintenant de calculer automatiquement des sommes ou des intégrales de fonctions très diverses. ... More
3 May 2009
Pedro Adao talks about High-Level Programming for E-Cash
Orsay, Bat I, 1st floor, MSR-INRIA Joint Centre, High-Level Programming for E-Cash Pedro Adão, Instituto Superior Técnico, Lisbon High-Level Programming for E-Cash E-cash protocols aim at providing robust abstractions for anonymous payment protocols. Properties of interest include, for instance, that users can spend coins anonymously, that users cannot forge coins, and that a user should.. ... More
22 April 2009
Giulio Manzonetto talks about Models and theories of the lambda calculus
Wednesday, April 22, 2009, 11h, bdg I, 1st floor, the MSR-INRIA Joint Centre, Inria Saclay, Models and theories of lambda calculus Giulio Manzonetto, INRIA A quarter of century after Barendregt’s main book, a wealth of interesting problems concerning denotational models and equational theories of the pure untyped lambda calculus are still open. In this talk.. ... More
8 April 2009
Thomas Ehrhard fait un exposé intitulé Logique linéaire différentielle, lambda-calcul et concurrence
8 avril 2009, 11h Orsay, Bat I, 1er étage, Centre de Recherche commun INRIA-MSR Logique linéaire différentielle, lambda-calcul et concurrence Thomas Ehrhard, PPS, Paris 7 En logique linéaire, les exponentielles “!” et “?” donnent un statut logique aux règles structurelles (affaiblissement et contraction). Cela nécessite la présence de deux règles d’introduction: la ... More
11 February 2009
Alan Schmitt gives seminar on HOCore
11 février 2009, 11h Orsay, Bat I, 1er étage, Centre de Recherche commun INRIA-MSR HOCore Alan Schmitt INRIA Rhône-Alpes HOCore est un calcul de processus d’ordre supérieur très simple, correspondant au pi calcul d’ordre supérieur sans la restriction. Ce calcul a la particularité d’être Turing Complete tout en ayant une équivalence observationnelle décidable. Nous présenterons.. ... More
4 February 2009
Colin Riba talks about Type-based termination with sized products
Type-based termination with sized products Colin Riba, ENS-Lyon, 4 February 2009, 13h30 Bldg I, ground floor Joint Work with Gilles Barthe (IMDEA - Madrid) and Benjamin Grégoire (INRIA Sophia Antipolis) Type-based termination is a semantically intuitive method that ensures termination of recursive definitions by tracking the size of datatype elements, and by checking that recursive.. ... More
16 January 2009
Rustan Leino talks about Correct Concurrency with Chalice
Friday, January 16, 2009, 11h, bdg I, 1st floor, the MSR-INRIA Joint Centre, Inria Saclay, Correct Concurrency with Chalice, Rustan Leino, Microsoft Research, Redmond, Chalice is an experimental language for writing and verifying concurrent programs using shared memory and mutual exclusion via locks. The semantic model for the language uses fractional permissions that can be.. ... More
15 January 2009
Rustan Leino gives a Digiteo conference on the Verification tools at Microsoft
Verification tools at Microsoft Rustan Leino, Microsoft Research, Redmond 15 January 2009, 10h30 Amphi du PUIO, bât 640, Université Paris-Sud Program verification and other symbolic-execution and static-analysis techniques are being explored and applied to software at Microsoft. In this talk, I will first describe and give a demo of Spec#, an experimental programming system that.. ... More