Events

Archives

Share:
A A
12 June 2006
TYPES Workshop on Numbers and Proofs
This workshop is part of the TYPES working group. It was organized by Benjamin Werner, Laurent Thery and Benjamin Gregoire ... More
12 June 2006
4 seminars on maths components
June 12th 2006 10:00am Henk Barendregt (Radboud University, Nijmegen) Progress in Computer MathematicsProgress in the foundations of mathematics has made it possible to formulate all thinkable mathematical concepts, algorithms and proofs in one language and in an impeccable way. This not in spite of, but partially based on the famous results of Gödel and Turing. In this.. ... More
9 June 2006
4 seminars on proofs and specs
June 9th 2006 10:00am Jean-Raymond Abrial (ETH Zurich) Functions and Capabilities of a Theorem Prover to be Used in the Modelling and Implementation of Complex Discrete Systems.In this presentation, I shall describe our experience in designing and using theorem provers for modelling and later implementing complex discrete systems. First, I shall draw the initial picture by showing.. ... More
2 June 2006
5 seminars on security (Blanchet, Barthe, Corin, Fournet, Lévy)
June 2nd 2006 10:00am Bruno Blanchet (CNRS, ENS Ulm) A Computationally Sound Mechanized Prover for Security ProtocolsWe present a new mechanized prover for secrecy properties of cryptographic protocols. In contrast to most previous provers, our tool does not rely on the Dolev-Yao model, but on the computational model. It produces proofs presented as sequences of games; these.. ... More
15 May 2006
Zhengyou Zhang, MSR Redmond, Microsoft Research and Selected Activities in Multimedia, HCI and RTC
Zhengyou Zhang (MSR Redmond) Microsoft Research and Selected Activities in Multimedia, HCI and RTCI will start with a brief introduction to Microsoft Research (MSR): its missions, how it functions, and the research activities in the Redmond center. I will then present some of my own research activities. I have been doing research in computer vision,.. ... More
27 February 2006
First meeting of the Management Committee
More
13 February 0207
2 seminars on theorem proving by Russel O’Connor and Enrico Tassi
Learning coq by proving the Godel’s incompleteness theorem, Russell O’connor University of Nijmegen, 11h The matita proof assistant and its disambiguation manager, Enrico Tassi, Joint Centre and Univ. of Bologna, 13h. Matita is a proof assistant developed at the university of bologna that integrates some technologies developed in the mkm (mathematical knowledge management) context. i.. ... More