Events

Archives

Share:
A A
9 July 2012
Russel O’Connor speaks about Galois Connections, Poset-Enriched Categorical Logic, and Type Theory.
Monday 9 July 2012, 14h Microsoft Research - Inria Joint Centre Campus de l’Ecole polytechnique, Palaiseau Bld Alan Turing, Salle MilnerSome Thoughts on Galois Connections, Poset-Enriched Categorical Logic, and Type Theory McMaster Univ. & MSR-Inria Joint CentreIn this talk I will present three bits of mathematics that have recently piqued my interest:- The first item.. ... More
27 June 2012
Eli Gafni speaks about Asynchrony from Synchrony
Microsoft Research - Inria Joint Centre Campus de l’Ecole polytechnique, Palaiseau Bld Alan Turing, Salle Grace HopperAsynchrony from Synchrony Eli Gafni, UCLA CSIn the past adversaries that reduce the computational power of a system as they become more powerful, were investigated in the context of asynchronous shared-memory. The adversary’s power was characterized by the set.. ... More
5 June 2012
The Joint Centre moves to Digiteo building in Polytechnique.
June 5, 2012 The Joint Centre moves to the new Digiteo bldg on the Campus of Polytechnique. See contact page ... More
9 May 2012
Timothy Griffin speaks about Routing in Equilibrium (with help from ssreflect)
Wednesday 9 May 2012, 11h Bldg I, 1st floor Microsoft Research - Inria Joint Centre Parc Orsay UniversitéRouting in Equilibrium (with help from ssreflect) Timothy G. Griffin , University of CambridgeSome path problems cannot be modelled using semirings because the associated algebraic structure is not distributive. Rather than attempting to compute globally optimal paths with.. ... More
4 May 2012
Karthikeyan Bhargavan defends his HDR (Habilitation)
Friday 4 May 2012, 11h Salle W, École Normale Supérieure 45, rue d’Ulm, 75005 — ParisTowards the Automated Verification of Cryptographic Protocol Implementations Karthikeyan Bhargavan INRIA — Paris Rocquencourt Abstract: In recent years, the emergence of effective protocol analyzers and expressive cryptographic models have enabled the proof of large cryptographic protocols, such as ... More
3 May 2012
Maxime Denes speaks about Effective algebra with Coq and SSReflect.
Bldg I, 1st floor Microsoft Research - Inria Joint Centre Parc Orsay Université Effective algebra with Coq and SSReflect Maxime Dénès (Marelle research team) Inria Sophia-Antipolis Proof assistants like Coq provide a unified framework to describe the implementation of algorithms and their proofs of correctness. Using such a tool to formalize computer algebra algorithms seems.. ... More
Levy (2)
4 April 2012
Cocktails party at Rocquencourt to celebrate retirement of Jean-Jacques Levy
JJ Retirement party INRIA Rocquencourt See nice photos (courtesy of Francois Pottier) More
8 February 2012
Jeremy Planul defends his PhD at Ecole polytechnique
Amphi Pierre Faurre Ecole polytechnique Using Cryptography For Multiparty Security Dissertation defence by Jérémy Planul, MSR-INRIA Joint Centre We are more and more dependent on our computing infrastructure, and yet its security is challenged every day. From a research viewpoint, a lot of progress in security has been made, using in particular formal methods and.. ... More
7 February 2012
P.Anandan speaks about Preservation of Cultural Heritage and General Research at Microsoft-Research India
INRIA, Antenne Italie 23 avenue d’Italie, 75013 Paris Preservation of Cultural Heritage and Research at Microsoft Research India P.Anandan P.Anandan is Managing Director of MSR India, Bangalore ... More
18 January 2012
Chantal Keller speaks about A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
Bldg I, 1st floor Microsoft Research - Inria Joint Centre Parc Orsay Université Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses Chantal Keller, LIX (Typical) In this talk, I will present a way to enjoy the power of SAT and SMT provers in Coq without compromising soundness. This requires these provers to return.. ... More