WoLLIC 2012 

19th Workshop on Logic, Language, Information and Computation 

September 3rd to 6th, 2012

University of Buenos Aires
Buenos Aires, Argentina

Scientific Sponsorship
Interest Group in Pure and Applied Logics (IGPL)
The Association for Logic, Language and Information (FoLLI)
Association for Symbolic Logic (ASL)
European Association for Theoretical Computer Science (EATCS)
European Association for Computer Science Logic (EACSL)
Sociedade Brasileira de Computação (SBC)
Sociedade Brasileira de Lógica (SBL)

Organisation
Departamento de Computación, Universidad de Buenos Aires, Argentina
Centro de Informática, Universidade Federal de Pernambuco, Brazil 

Title and Abstracts of Invited Talks

Formalizing Turing Machines

Andrea Asperti and Wilmer Ricciotti, University of Bologna, Italy

We discuss the formalization, in the Matita Theorem Prover, of a few, basic results on Turing Machines, up to the existence of a (certified) Universal Machine. The work is meant to be a preliminary step towards he creation of a formal repository in Complexity Theory, and is a small piece in our Reverse Complexity program, aiming to a comfortable, machine independent axiomatization of the field.

Admissible Rules: From Characterizations to Applications

Geoge Metcalfe, University of Bern, Switzerland

The admissible rules of a logic (understood as a consequence relation) can be described, equivalently, as rules that can be added to the logic without producing any new theorems, and also as rules such that any substitution making the premises into theorems, also makes the conclusion into a theorem. However, this equivalence collapses once multiple-conclusion or other, more exotic, admissible rules are considered. The first aim of this talk will be to explain how such distinctions can be explained and characterized. The second will be to show how the admissibility of rules, often established using syntactic eliminations, can be useful in characterizing properties of classes of algebras. 

On distributed control and monitoring

Anca Muscholl, LaBRI, Université Bordeaux, France

In this survey we discuss verification issues in the setting of distributed finite-state systems. Verifying the correctness of such systems is known to be a very challenging task, for which current techniques are much less advanced than for sequential systems. First we will consider the control problem for finite-state processes synchronizing via shared variables, a particular instance of distributed synthesis. Its decidability status is one the main open problems in this area. Then we consider the monitoring problem, where we are interested in properties that can be monitored locally on such systems. We propose a  distributed framework for monitoring issued from topological considerations.

This is joint work with Volker Diekert (Univ. of Stuttgart, Germany)

Logical methods in quantum information theory

Peter Selinger, Dalhousie University, Canada

I will talk about some recent applications of logical methods to quantum information theory. In computing, a higher-order function is a function for which the input or output is another function. I will argue that many of the interesting phenomena of quantum information theory involve higher-order functions, although that is not how they are usually presented. I'll talk about the quantum lambda calculus as a possible framework to describe such phenomena.

Last modified: May 15, 2012 07:53am GMT-3.