LSFA 2012 - 7th Workshop on Logical and Semantic Frameworks, with Applications
LSFA 2012 - 7th Workshop on Logical and Semantic Frameworks, with Applications

Invited speakers CFP Important dates Program Committee Organization Sponsors

Registration Venue LSFA bus Accommodations Program Poster Contact

new Photos new

LSFA 2012 - 7th Workshop on Logical and Semantic Frameworks, with Applications

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.

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.

In this seventh edition, the workshop will be in September 29-30 in Rio de Janeiro, at Pontifícia Universidade Católica do Rio de Janeiro (PUC-Rio).

The previous editions of this conference were held in Belo Horizonte (2011), Natal (2010), Brasilia (2009), Salvador (2008), Ouro Preto (2007), Natal (2006).

Download LSFA 2012 poster: LSFA_2012_poster.pdf

LSFA bus

LSFA 2012 organization is providing a bus from Argentina Hotel to the venues where the event will take place. To use this transportation, you should have be registered.

LSFA bus (exclusive transportation for LSFA attendees) schedule:

  • Saturday, 08:00 - from Argentina Hotel to PUC-Rio
  • Saturday, 20:00 - from PUC-Rio to Argentina Hotel
  • Sunday, 08:00 - from Argentina Hotel to MAC-Niterói
  • Sunday, 14:00 - from MAC-Niterói to Argentina Hotel

For more information please contact the chairs:

  • Renata de Freitas (renatafreitas at
  • Petrucio Viana (petrucio at


LSFA 2012 will be held at Pontifícia Universidade Católica do Rio de Janeiro (PUC-Rio), on Saturday (September, 29th) and at MAC Niterói, on Sunday (September, 30th):

  • Saturday (September, 29th) - PUC-Rio
    • 09:00/16:20 - RDC Auditorium (RDC Building)
    • 16:20/20:00 - "Sala do Decanato" (Cardeal Leme Building, 12th floor)
  • Sunday (September, 30th) - MAC-Niterói
    • 09:00/14:00 - MAC Auditorium (next to "Bistrô MAC" - underground)

Map to PUC-Rio
Map to MAC-Niterói

In case you miss the LSFA bus:

  • The best option to go to PUC-Rio, from Flamengo (Argentina Hotel), by bus is to take 410 - Pça Saens Pena x Gávea, at Praia do Flamengo and get off at the final stop, at PUC-Rio. It takes 40min, approx. (12km).
  • The best option to go to MAC-Niterói, from Flamengo (Argentina Hotel), by bus is to take 750 D - Charitas x Gávea, via Túnel Santa Bárbara, at Senador Vergueiro Street, get off at Dr. Paulo Alves Street, and walk to MAC-Niterói (take the direction of the seashore and you will see the museum). It takes 1h, approx. (30km).

Here you can find out how to travel by bus in Rio de Janeiro state.

For more information please contact the chairs:

  • Renata de Freitas (renatafreitas at
  • Petrucio Viana (petrucio at


We advise people from outside Rio de Janeiro to stay at Flamengo, at one of the official hotels of LSFA 2012, with special daily rates for LSFA 2012 attendees:

  • Argentina Hotel (Rua Cruz Lima, 30, Flamengo)
    Daily rates:
    • Single - R$ 215,00 + 5%
    • Double - R$ 240,00 + 5%
    • Triple - R$ 304,00 + 5%
    • Quadruple - R$ 376,00 + 5%
  • Augusto's Paysandú Hotel
    Daily rates:
    • Single - R$ 198,00 + 5%
    • Double - R$ 220,00 + 5%
  • Cafofo Hostel
    Daily rates:
    • R$35 - daily rate for staying two nights, at least
    • R$38 - daily rate for staying only one night

For some information about visiting Rio de Janeiro, please visit:

For more information please contact the chairs:

  • Renata de Freitas (renatafreitas at
  • Petrucio Viana (petrucio at

Invited speakers

Torben Braüner (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 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-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.


The registration to the conference can be done here. The payment is via Paypal (credit cards accepted), and a notification with instructions will be sent via e-mail after the registration.

At least one of the authors of accepted papers should register at the conference.

Registration fees:

  • Early registration (payment until September 10th, 2012)
    • Student: R$ 130,00 or US$ 63
    • Regular: R$ 200,00 or US$ 97
  • Late registration (payment after September 10th, 2012)
    • Student: R$ 180,00 or US$ 88
    • Regular: R$ 250,00 or US$ 122

The registration fee includes coffee breaks and pre-proceedings.

LSFA 2012 - Registration Form



September 29th, 2012 - Saturday (PUC-Rio)

09:00 - 16:20
RDC Auditorium

09:00 - 09:20 Registration

09:20 - 09:30 Opening

09:30 - 10:20 Invited talk

  • Alexandre Miquel, A survey of classical realizability

10:20 - 10:45 Beniamino Accattoli, Proof nets and the call-by-value lambda-calculus

10:45 - 11:10 Coffee break

11:10 - 11:35 Alberto Carraro, Thomas Ehrhard and Antonino Salibra, The stack calculus

11:35- 12:00 Alberto Carraro, The untyped stack calculus and Bohm's theorem

12:00 - 14:00 Lunch

14:00 - 14:50 Invited talk

  • Edward Hermann Haeusler, A proof-theoretical discussion on the mechanization of propositional logics

14:50 - 15:50 EHH festschrit

Together with this edition of LSFA it will be held a celebration of the 50th birthday of Professor Edward Hermann Haeusler.

15:50 - 16:20 Coffee Break

16:20 - 20:00
"Sala do Decanato" (Cardeal Leme Building, 12th floor)

16:20 - 16:45 Alejandro Díaz-Caro and Gilles Dowek, Non determinism through type isomorphism

16:45 - 17:10 Daniele Nantes Sobrinho, Mauricio Ayala-Rincón and Maribel Fernández, Elementary Deduction Problem for Locally Stable Theories with Normal Forms

17:10 - 17:35 Carlos Areces, Guillaume Hoffman and Ezequiel Orbe, Symmetries in Modal Logics: A Coinductive Approach

17:35 - 18:00 Alberto Carraro, Antonino Salibra and Antonio Bucciarelli, Minimal lambda-theories by ultraproducts

Social event

September 30th, 2012 - Sunday (MAC-Niterói)

09:00 - 14:00
MAC Auditorium (next to "Bistrô MAC", underground)

09:00 - 09:50 Invited talk

  • Torben Braüner, Hybrid Logic and its Proof-Theory

09:50 - 10:15 Marcelo Coniglio and Maria Corbalán, Sequent Calculi for the conjunction-negation fragment of Bochvar and Halldén's Nonsense Logics

10:15 - 10:40 Paulo Veloso and Sheila Veloso, A Graph Calculus for Predicate Logic

10:40 - 11:10 Coffee break

11:10 - 11:35 Alberto Ciaffaglione and Ivan Scagnetto, A weak HOAS approach to the POPLmark Challenge

11:35 - 11:50 Ana Cristina Rocha Oliveira and Mauricio Ayala-Rincón, Formalizing the Confluence of Orthogonal Rewriting Systems

11:50 - 12:40 Invited talk

  • Maribel Fernández, A framework to specify access control policies in distributed environments

12:40 - 12:50 Closing

Business meeting lunch

Call for Papers

Topics of interest to this forum include, but are not limited to:

  • Logical frameworks
  • Proof theory
  • Type theory
  • Automated deduction
  • Semantic frameworks
  • Specification languages and meta-languages
  • Formal semantics of languages and systems
  • Computational and logical properties of semantic frameworks
  • Implementation of logical and/or semantic frameworks
  • Applications of logical and/or semantic frameworks

LSFA 2012 also aims to be a forum for presenting and discussing work in progress, and therefore to provide feedback to authors on their preliminary research.

The proceedings are produced only after the meeting, so that authors can incorporate this feedback in the published papers.

Contributions should be written in English and submitted in the form of full papers (with a maximum of 16 pages) or short papers (with a maximum of 6 pages). They must be unpublished and not submitted simultaneously for publication elsewhere. The papers should be prepared in latex using EPTCS style. The submission should be in the form of a PDF file uploaded to LSFA 2012 page at Easychair, until the (extended) submission deadline in June 22th, by midnight, Central European Standard Time (GMT+1).

The workshop pre-proceedings, containing the reviewed extended abstracts, will be handed-out at workshop registration.

After the workshop the authors will be invited to submit full versions of their works for the post-proceedings to be published in EPTCS.

At least one of the authors should register at the conference.

The paper presentation should be in English.

Important Dates
  • Paper submission deadline: June 22th, 2012 (extended)
  • Author notification: July 22th, 2012 (extended)
  • Camera-ready: August 12th, 2012 (extended)
  • Conference: September 29-30, 2012

Program Committee
  • Carlos Areces (Univeridad Nacional de Córdoba, 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)
  • Hermann Haeusler (PUC-Rio, Brazil)
  • Delia Kesner (Université Paris Diderot, France) (co-chair)
  • Luis da Cunha Lamb (UFRGS, Brazil)
  • Ian Mackie (École Polytechnique, France)
  • Joao Marcos (UFRN, Brazil)
  • Georg Moser (University of Innsbruck, Austria)
  • Koji Nakazawa (Kyoto University, Japan)
  • Vivek Nigam (Ludwig-Maximilians-Universität München, Germany)
  • Luca Paolini (Università di Torino, Italy)
  • Elaine Pimentel (Univalle, Colombia)
  • Simona Ronchi Della Rocca (Università di Torino, Italy)
  • Maurício Ayala-Rincón (UnB, Brazil)
  • Luis Menasche Schechter (UFRJ, Brazil)
  • Sheila Veloso (UERJ, Brazil)
  • Daniel Ventura (UFG, Brazil)
  • Petrucio Viana (UFF, Brazil) (co-chair)

  • 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)
  • Maurício Ayala-Rincón (UnB, Brazil) (co-chair)


Gallery of Photos

Every attendee is invited to share photos taken during LSFA 2012.
If you want to do so, please contact Renata de Freitas (renatafreitas at
Here are some that we already received:

  • By Danilo Souza

    At PUC-Rio, September 29th
    At MAC-Niterói, September 30th
  • By Alberto Ciaffaglione

    At MAC-Niterói, September 30th

  • By Alejandro Días-Caro

    At PUC-Rio, September 29th
    At MAC-Niterói, September 30th


Contact Information

For more information please contact the chairs:

  • Renata de Freitas (renatafreitas at
  • Petrucio Viana (petrucio at




Last edited - October 11th (by Renata de Freitas)