13th Workshop on Logic, Language, Information and Computation

July 18th to 21st, 2006

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)

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

Center for Latin American Studies, Stanford University
Department of Philosophy, Stanford University
CSLI, Stanford University

Title and Abstracts of Tutorial Lectures

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.

Behavioral Computation Theory: Tutorial
by Yuri Gurevich (Microsoft Research, USA)

Classical computation theory, including computational complexity theory, was a great advance in the study of algorithms but the theory has severe limitations that make it inadequate for modern engineering. In particular, the behavior of an algorithm is restricted to the input/output relation, and inputs are supposed to be string-codable. Behavioral computation theory, aka the theory of abstract state machines, overcomes these restrictions. We explain the basics of behavior computation theory and mention various applications. For those who want to do a little reading ahead of time, the best place to start is article #141 at speaker's webpage. For a broad-brush picture see #164 and #174. For those who have a greater appetite for reading and who are unafraid of technical details, there are articles #157, #166, #170, #171, #176.

Proof Mining: Applications of Proof Theory to Analysis
by Ulrich Kohlenbach (Department of Mathematics, Darmstadt University of Technology, Germany)

In recent years (though influenced by papers of G. Kreisel going back to the 50's) an applied form of proof theory systematically evolved with sometimes is called "Proof Mining". This approach is concerned with the extraction of both new effective data as well as new qualitative information (independence of solutions from certain parameters) from typically ineffective proofs. A particularly fruitful area of applications has been functional analysis. This 2-part tutorial will give a survey on the logical background and applications of this approach.

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, 11:02am PST.