Center for the Study of Language and Information (CSLI), Stanford, California, USA
Scientific Sponsorship
Interest Group in Pure and Applied Logics (IGPL)
European Association for Logic, Language and Information (FoLLI)
Association for Symbolic Logic (ASL)
European Association for Theoretical Computer Science (EATCS)
Sociedade Brasileira de Computação (SBC)
Sociedade Brasileira de Lógica (SBL)
Funding
The Tinker Foundation
The Office of the Provost, Stanford University
CSLI, Stanford University
Department of Philosophy, Stanford University
Dept of Mathematics, Stanford University
Symbolic Systems Program, Stanford University
Organisation
Center for Latin American Studies, Stanford University
Department of Philosophy, Stanford University
CSLI, Stanford University
New insights into Probabilistically Checkable Proofs (PCPs)
by
Eli Ben-Sasson (Comput Sci Dept, Technion Inst of Technology, Israel)
We revisit the celebrated PCP Theorem in light of recent simplifications to its proof and discuss new applications to error correcting codes and sub-linear time proof verification.
Reminder: The celebrated PCP Theorem was proved in the early 1990's [Arora,Safra;Arora,Lund,Motwani,Sudan,Szegedy]. Informally speaking, it says there is a format of writing proofs and a probabilistic method of verifying their correctness. In this method the verifier needs to read only a constant number of random bits from the proof (independent of the proof length) to test its validity. Good proofs of true statements are accepted with probability one, whereas any purported "proof" of a false statement is rejected with probability of at least one third.
Operational theories of sets
by
Solomon Feferman (Depts of Mathematics and Philosophy, Stanford University, USA)
In a kind of extension of von Neumann's axiomatization (VN) of set theory with functions at the level of classes, the language of set theory is here augmented by variables for operations in an untyped partial combinatory algebra over sets. Like the earlier approach, this language lends itself to a more natural formulation of standard set-theoretical axioms, such as those of Replacement and Choice as well as the usual closure conditions on sets. But the present formalism also has the advantage of much greater freedom than the VN approach since it permits the representation of higher order closure conditions. In particular, operational set theory is applied to obtain unified formulations of various "small" large cardinal axioms (i.e., those consistent with V=L), such as Mahlo, weakly compact, etc., in terms that are abstractly the same whether in usual set theory with the power-set operation or admissible set theory without it. The latter replaces analogue formulations in terms of recursive functions on admissible sets and schematic reflection principles.
The expanding notion of algorithm
by
Yuri Gurevich (Microsoft Research, USA)
The notion of algorithm is key in computer science. Computer programs are algorithms. This includes e.g. operating systems. Programming languages themselves can be viewed as universal algorithms that treat a particular program as part of input. A foundational problem arises: What is an algorithm? But the notion of algorithm expands and deepens as the computer revolution advances. In addition to classical sequential algorithms, we have now concurrent algorithms, distributed algorithms, real-time algorithms. Algorithms grow in size and complexity raising numerous software concerns like fault tolerance and maintainability. The variety of algorithms is bewildering. The foundational problem may seem hopeless. And yet there has been a substantial progress in the area, partially covered in our WoLLIC 2006 tutorial. Here we concentrate on issues that are not covered in the tutorial, in particular on distributed algorithms and on the question what the notion of algorithm is in its full generality. To what extent one can anticipate the limit point of the expansion of the notion of algorithm?
A logical uniform boundedness principle for
abstract metric and hyperbolic spaces
by
Ulrich Kohlenbach (Department of Mathematics, Darmstadt University of Technology, Germany)
This talk will present some of the most recent applications of logical metatheorems developed in the course of proof mining to functional analysis. We will also discuss some new proof theoretic results which were prompted by these applications. This includes a powerful "nonstandard" uniform boundedness principle for abstract metric and hyperbolic spaces.
(tba)
by
Thomas Scanlon (Mathematics Department, University of California at Berkeley, USA)
Symbolic Analysis of Computer Network Security Protocols
by
Andre Scedrov (Department of Mathematics, University of Pennsylvania, USA)
While modern cryptography relies on applications of number theory, probability theory, and computational complexity, the methods of symbolic logic are contributing in significant ways to the wider area of computer security, including network security, access control, and policy languages. We will explore some of the applications of the abstract symbolic methods in these areas and in particular in the analysis of network security protocols. We will also consider several ways in which abstract symbolic methods relate to mathematical applications in cryptography.
As an example of this methodology we describe joint work with I. Cervesato, A.D. Jaggard, J.-K. Tsay, and C. Walstad on a vulnerability in PKINIT, the public key extension of the widely deployed Kerberos 5 authentication protocol. The discovery of this flaw caused an internet standards body IETF to change the specification of PKINIT and caused Microsoft to release a security update for a number of Windows operating systems. A Microsoft Security Bulletin which mentions this work is available on http://www.microsoft.com/technet/security/bulletin/MS05-042.mspx We discovered this flaw as part of an ongoing symbolic analysis of the Kerberos protocol suite, and we have verified in the symbolic model several fixes to PKINIT that prevent our attack.
Last modified: May 24, 2006, 10:57am PDT.