[TYPES/announce] LSFA 2012 - Call for participation

[Christiano Braga]

======================================================================
[ please distribute - apologies for multiple copies ]
======================================================================

LSFA 2012 - Call For Participation

7th Workshop on Logical and Semantic Frameworks, with Applications

Rio de Janeiro, Brazil
September 29-30, 2012
http://www.uff.br/lsfa/


Logical and semantic frameworks are formal languages used to represent
logics, languages and systems. These frameworks provide foundations
for formal specification of systems and programming languages,
supporting tool development and reasoning.

In its seventh edition, the workshop will be at Pontificia
Universidade Católica do Rio de Janeiro (PUC-Rio). Previous editions
of this conference were held in Belo Horizonte (2011), Natal (2010),
Brasilia (2009), Salvador (2008), Ouro Preto (2007), Natal (2006).

The objective of this workshop is to put together theoreticians
and practitioners to promote new techniques and results, from the
theoretical side, and feedback on the implementation and the use of
such techniques and results, from the practical side.

Together with this edition it will be held a celebration of the
50th birthday of Professor Professor Edward Hermann Haeusler on
Saturday September 29th, 2012.


Important Dates

Early registration deadline: September 10th, 2012
Conference: September 29-30, 2012


Invited talks

* Torben Brauner (Roskilde University, Denmark)

Hybrid Logic and its Proof-Theory

Hybrid logic is an extension of ordinary modal logic which allows
explicit reference to individual points in a model (where the points
represent times, possible worlds, states in a computer, or something
else). This additional expressive power is useful for many applications,
for example when reasoning about time one often wants to formulate
a series of statements about what happens at specific times.

There is little consensus about proof-theory for ordinary modal logic.
Many modal-logical proof systems lack important properties and the
relationships between proof systems for different modal logics are
often unclear. In my talk I will demonstrate that these deficiencies
are remedied by hybrid-logical proof-theory.

In my talk I first give a brief introduction to hybrid logic and its origin
in Arthur Prior's temporal logic. I then describe essential
proof-theoretical results for a natural deduction formulation of
hybrid logic. The natural deduction system is extended with additional
inference rules corresponding to conditions on the model expressed by
what are called geometric theories. Thus, I give natural deduction
systems in a uniform way for a wide class of hybrid logics.


* Maribel Fernández (King's College London, UK)

A framework to specify access control policies in distributed environments.

In this talk, we present a meta-model for access control that takes
into account the requirements of distributed environments, where
resources and access control policies may be distributed across
several sites. This framework extends the ideas underlying Barker's
category-based meta-model. We use term rewriting to give an
operational semantics to the distributed meta-model, and then show
how various distributed access control models (e.g., MAC, DAC, RBAC,
Bell-Lapadula) can be derived.can be as instances of the meta model.

Based on work done jointly with Clara Bertolissi.


* Edward Hermann Haeusler (PUC-Rio, Brazil)

A proof-theoretical discussion on the mechanization of
propositional logics

The computational complexity of SAT and TAUT for purely implicational
propositional logic is known to be PSPACE-complete. Intuitionistic
Propositional Logic is also known to be PSPACE-complete, while
Classical Propositional Logic is CONP-complete for Tautology checking
and NP-complete for Satisfiability checking. We show how
proof-theoretical results on Natural Deduction help analysing the
Purely Implicational Propositional Logic complexity regarded its
polynomial relationship to Intuitionistic and Classical Propositional
Logics. The main feature in this analysis is the sub-formula
principle property. We extended the polynomial reduction of purely
implicational logic to any propositional logic satisfying the
sub-formula principle. Hence, any propositional logic satisfying the
sub-formula principle is in PSPACE. We conclude that some well-known
logics, such as Propositional Dynamic Logic and S5C (n = 2), for
example, hardly satisfy the sub-formula property. On the other hand,
these logics have proof procedures. They are told to be mechanizable
despite being EXPTIME-complete.

We point out some facts and discuss some questions on how the
sub-formula property is related to the mechanization of theorem
proving for propositional logics. The relationship between feasible
interpolants and the sub-formula property is discussed. Some examples
remind us that the relationship between normalization of proofs and
the sub-formula property is weak. Finally we discuss some alternative
criteria to consider a logic to be mechanizable. This discussion is
strongly influenced by A. Carbone analysis on propositional proof
complexity. Our purpose is to show how structural proof theory can
help us in analysing hard relationships on propositional logic
systems.


* Alexandre Miquel (ENS de Lyon, France)

A survey of classical realizability

The theory of classical realizability was introduced by Krivine in
the middle of the 90's in order to analyze the computational contents
of classical proofs, following the connection between classical
reasoning and control operators discovered by Griffin.

More than an extension of the theory of intuitionistic realizability,
classical realizability is a complete reformulation of the very
principles of realizability based on a combination of Kleene's
realizability with Friedman's A-translation.

One of the most interesting aspects of the theory is that it is highly modular:
although it was originally developed for second order
arithmetic, classical realizability naturally extends to more
expressive frameworks such as Zermelo-Fraenkel set theory or the
calculus of constructions with universes. Moreover, the underlying
language of realizers can be freely enriched with new instructions in
order to realize extra reasoning principles, such as the axiom of
dependent choices. More recently, Krivine proposed an ambitious
research programme, whose aim is to unify the methods of classical
realizability with Cohen's forcing in order to extract programs
from proofs obtained by the forcing technique.

In this talk, I shall survey the methods and the main results of
classical realizability, while presenting some of its specific
problems, such as the specification problem. I shall also discuss
the perspectives of combining classical realizability with the
technique of forcing, showing that this combination is not only
interesting from a pure model theoretic point of view, but that it
can also bring new insights about a possible widening of the
proofs-as-programs correspondence beyond the limits of pure
functional programming.


Scientific Committee

* Carlos Areces (Univeridad Nacional de Cordoba, Argentine)
* Arnon Avron (Tel-Aviv University, Israel)
* Patrick Baillot (Ens de Lyon, France)
* Veronica Becher (Universidad de Buenos Aires, Argentine)
* Marcelo Coniglio (Unicamp, Brazil)
* Thierry Coquand (University of Gothenburg, Sweden)
* Hans van Ditmarsch (University of Sevilla, Spain)
* Clare Dixon (The University of Liverpool, UK)
* Marcelo Finger (IME-USP, Brazil)
* Edward Hermann Haeusler (PUC-Rio, Brazil)
* Delia Kesner (Universite Paris Diderot, France) (co-chair)
* Luis da Cunha Lamb (UFRGS, Brazil)
* Ian Mackie (Ecole Polytechnique, France)
* Joao Marcos (UFRN, Brazil)
* Georg Moser (University of Innsbruck, Austria)
* Koji Nakazawa (Kyoto University, Japan)
* Vivek Nigam (Ludwig-Maximilians-Universitat Munchen, Germany)
* Luca Paolini (Universita di Torino, Italy)
* Elaine Pimentel (Univalle, Colombia)
* Simona Ronchi Della Rocca (Universita di Torino, Italy)
* Mauricio Ayala-Rincon (UnB, Brazil)
* Luis Menasche Schechter (UFRJ, Brazil)
* Sheila Veloso (UFRJ, Brazil)
* Daniel Ventura (UFG, Brazil)
* Petrucio Viana (UFF, Brazil) (co-chair)


Organization

* Departamento de Ciência da Computação, UnB
* Departamento de Filosofia, Departamento de Informática, PUC-Rio
* Instituto de Matemática e Estatística, UFF


Organizing Committee

* Christiano Braga (UFF)
* Renata de Freitas (UFF) (co-chair)
* Luiz Carlos Pereira (PUC-Rio, UFRJ)
* Mauricio Ayala-Rincon (UnB) (co-chair)

======================================================================