====================================================================== [ 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) ====================================================================== _______________________________________________ Logica-l mailing list [email protected] http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
