CHAIRE ANDRÉ AISENSTADT CHAIR 2010
Une série de conférences / A series of lectures

Yuri Gurevich (Microsoft Research)


yuri
Yuri Gurevich

Photos de la conference / Conference photos

Telecharger l'affiche / Download poster


Lundi 13 septembre 2010, 16h00
Monday, September 13, 2010, 4:00 pm

Centre de recherches mathématiques
Pavillon André-Aisenstadt, Université de Montréal
2920, ch. de la Tour , Salle / Room 1355

Cette conférence s'adresse à un large auditoire / Suitable for a general audience

The Church-Turing Thesis: Story and Recent Progress

The Church-Turing thesis is one of the foundations of computer science. The thesis heralded the dawn of the computer revolution by enabling the construction of the universal Turing machine which led the way, at least conceptually, to the von Neumann computer architecture and first electronic computers. The thesis says that every numerical function computable by means of a purely mechanical procedure is computable by a Turing machine. It is that remarkable and a priori implausible characterization that underlies the ubiquitous applicability of digital computers.

But why do we believe the thesis? It is not hard to see that the existing arguments in favor of the thesis are insufficient. Kurt Goedel surmised that it might be possible to state axioms which embody the generally accepted properties of computability, and then to prove the thesis on that basis. That is exactly what we did in a recent paper with Nachum Dershowitz of Tel Aviv University.

The story of the Church-Turing thesis is fascinating and scattered in specialized and often obscure publications. We will try to do justice to that intellectual drama.

Une réception suivra la conférence au Salon Maurice-L'abbé, Pavillon André-Aisenstadt (Salle 6245).
There will be a reception after the lecture in Salon Maurice-L'abbé, Pavillon André-Aisenstadt (Room 6245).

Mardi 14 septembre 2010, 16h00
Tuesday, September 14, 2010, 4:00 pm

Centre de recherches mathématiques
Pavillon André-Aisenstadt, Université de Montréal
2920, ch. de la Tour , Salle / Room 6214

Security Policy: Logic and Engineering

In software industry, a useful formalization of the problem at hand is much more likely to involve logic rather partial differential equations. Many engineers do formal logic day and day out even though they may not realize that. Security policy is one of those fields where engineers do logic. The security policy of a large organization is complex all by itself. It is hard to keep it consistent. But the organization does not live in vacuum. Imagine a paranoid world where trust is in short supply but interaction is extensive and should be automated. To this end we created a policy language called Evidential DKAL (where DKAL stands for Distributed Knowledge Authorization Language). In the lecture we will present this piece of applied logic and touch on the issue of real-world computability.

 

Jeudi 16 septembre 2010, 16h00 /
Thursday, September 16, 2010, 4:00 pm

Centre de recherches mathématiques
Pavillon André-Aisenstadt, Université de Montréal
2920, ch. de la Tour , Salle / Room 6214

What, if anything, can you do in linear time?

In mathematics and theoretical computer science, it is often claimed that polynomial time is feasible. Is this true? Well that depends, on the application and on the polynomial. Some applications require linear time solutions. A problem of size n should be solved in cn time where c is reasonably small. But what can you do in linear time? More than one may expect. We describe some problems that are, unexpectedly, solvable in linear time.

We came across linear time computability working on logics relevant to security policies. We motivate and describe a particular logic L relevant to security policies and show that the following problem is solvable in linear time: given sequence H of hypotheses H and a sequence Q queries, determine which queries follow from the hypotheses.