LSFA 2014 - 9th Workshop on Logical and Semantic Frameworks, with Applications

Photo - Ipe

8-9 September 2014, Brasília D.F., Brazil

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 bring together theoreticians and practitioners to promote new techniques and results, and to facilitate feedback on the implementation and application of such techniques and results in practice. 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 2014 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 after the meeting, so that authors can incorporate this feedback in the published papers.

LSFA 2014 will take place on the 8th and 9th September 2014 in Brasilia. Previous editions took place in Sao Paulo (2013), Rio de Janeiro (2012), Belo Horizonte (2011), Natal (2010), Brasilia (2009), Salvador (2008), Ouro Preto (2007) and Natal (2006). More information about the workshop series can be found by clicking here.

Grants for Students

  • Wednesday, August 27 -     Deadline for applications and recommendation letters
  • Friday, August 29 -      Notification

Call for 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 ENTCS style. The submission should be in the form of a PDF file uploaded to Easychair:

The pre-proceedings, containing the reviewed extended abstracts, will be handed-out at event registration. After the meeting the authors will be invited to submit full versions of their works for the post-proceedings to be published in ENTCS. At least one of the authors should register for the conference. Presentations should be in English.

Important dates

Invited Speakers

Ugo Montanari (University of Pisa, Italy)

Title: Network-Conscious pi-Calculus - A model of Pastry - Joint work with Matteo Sammartino.

Abstract: A peer-to-peer system provides the networking substrate for the execution of distributed applications. It is made of peers that interact over an application-level overlay network, built on top of the physical one. An overlay network is highly dynamic, as peers can join and leave it at any time, and this causes continuous reconfigurations of its topology.
Traditional process calculi, such as CCS, pi-calculus and others, seem inadequate to describe these kinds of networks, their routing mechanisms, and to verify their properties. In fact, they abstract away from network details, as two processes are allowed to communicate only through shared channels. In order to model network architecture in a more explicit way, we have introduced the Network Conscious Pi-calculus (NCPi), a seamless extension of the pi-calculus with a natural notion of network: nodes and links are regarded as computational resources that can be created, passed and used to transmit. Conveniently, NCPi is equipped with a coalgebraic semantics on a presheaf category, where indexes, i.e. free names, represent nodes and links of the available network.
In this talk we introduce NCPi and present a NCPi model of the p2p architecture Pastry. In Pastry, peers have unique identifiers, logically ordered in a ring. The main operation is routing by key: given a message and a target key, the message is delivered to the peer whose identifier is numerically closest to the key. Pastry is typically used for implementing Distributed Hash Tables (DHT), that are hash tables whose entries are distributed among peers: routing by key in this context amounts to hash table lookup.

Andrew M Pitts (University of Cambridge, England)

Title: Constructive Type Theory with Abstractable Names.

Abstract: Nominal sets provide a mathematical theory of structures involving names and binding constructs, based on some simple, but subtle ideas going back to Fraenkel and Mostowski's symmetric models of set theory with atoms. The theory has been applied to programming language semantics, machine-assisted theorem proving and the design of functional and logical metaprogramming languages. In this talk the speaker want to discuss the extension of logical frameworks based on dependent types (and dependently typed functional programming) with features that are modelled by the nominal sets notion of name abstraction. What is the motivation for such an extension? What ways of doing it have been tried so far? What are their shortcomings and can they be overcome? These are some of the questions the speaker hope to address.

René Thiemann (Universität Innsbruck, Austria)

Title: A Framework for Developing Stand-Alone Certifiers.

Abstract: Current tools for automated deduction are often powerful, but their complexity implies the risk of containing bugs and thus deliver wrong results. To ensure reliability of these tools, one possibility is to develop certifiers which check the results of the tools with the help of some trusted theorem prover. We present a framework which illustrates the essential steps to develop stand-alone certifiers which efficiently check generated proofs outside the theorem prover. The applicability of our framework is demonstrated by the fact, that it has already been used to develop certifiers for various properties, including termination, confluence, completion, and tree automata related properties.

Program Committee

Elvira Albert (U. Complutense de Madrid, Spain)
Sandra Alves (U. de Porto, Portugal)
Sandra de Amo (UFU, Brazil)
Carlos Areces (U. Nacional de Cordoba, Argentina)
Mauricio Ayala-Rincon (UnB, Brazil -- co-chair)
Mario Benevides (UFRJ, Brazil)
Stefan Berghofer (secunet Security Networks AG, Germany)
Walter Carnielli (UNICAMP, Brazil)
Carlos Castro (UT Federico Santa Maria, Chile)
Adriana Compagnoni (Stevens Institute of Technology, USA)
Marcello D'Agostino (U Ferrara, Italy)
Maribel Fernandez (King's College London, England)
Marcelo Finger (IME-USP, Brazil)
Renata de Freitas (UFF, Brazil)
Simon Gay (University of Glasgow, Scotland)
Edward Hermann Haeusler (PUC-Rio, Brazil)
Fairouz Kamareddine (Heriot-Watt, Scotland)
Delia Kesner (U. Paris Diderot, France)
Luis Lamb (UFRGS, Brazil)
Ian Mackie (Ecole Polytechnique Palaiseau, France -- co-chair)
Joao Marcos (UFRN, Brazil)
Cesar Munoz (NASA LaRC, USA)
Vivek Nigam (UFPB, Brazil)
Elaine Pimentel (UFMG, Brazil)
Renata Hax Sander Reiser (UFPel, Brazil)
Femke van Raamsdonk (U. Amsterdam, Holland)
Simona Ronchi Della Rocca (U. Torino, Italy)
Carolyn Talcott (SRI International, USA)
Alvaro Tasistro (U. ORT, Uruguay)
Daniel Ventura (UFG, Brazil)
Jorge Petrucio Viana (UFF, Brazil)
Renata Wassermann (IME-USP, Brazil)
Tjark Weber (Uppsala University, Sweden)

Organising Committee

Flávio L. C. de Moura (UnB, Brazil)
Daniele Nantes Sobrinho (UnB, Brazil)
Home page:


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

Early registration (payment until August 25th, 2014)

Student: R$ 220,00 or U$100,00
Regular: R$ 330,00 or U$150,00

Late registration (payment from August 26th, 2014 on)

Student: R$260,00 or U$ 120,00
Regular: R$400,00 or U$ 180,00

  • Brazilian participants must pay by bank transfer for early or late registration or in cash for on site registration.

  • Foreigners should register on the conference, however, they may pay in cash on the arrival at the meeting.

  • If you have any questions, please send an email to

    Bank Details

    Banco do Brasil
    Agência: 2936-x
    Conta-Corrente: 16.145-4
    Nome: Daniele Nantes Sobrinho

    To register (foreigners and brazilians), please send an email to with the following information:

    • Name
    • Affiliation
    • Student or Regular?
    • Date of Arrival/Departure
    • Copy of the bank deposit (except foreigners)

    We will confirm the registration within 3 days.


    We suggest the following hotels in the area called Setor Hoteleiro Norte, it is well located, close to Brasília Shopping, Pátio Brasil Shopping and other restaurants.
    Saint Moritz
    Setor Hoteleiro Norte(SHN), Quadra 1, Área Especial A, Bloco B
    Postcode: 70701-000, Brasília, Brazil
    Monumental Bittar
    Setor Hoteleiro Norte(SHN), Quadra 3, Bloco B
    Postcode: 70702-912, Brasília, Brazil.
    Aristus Hotel
    Setor Hoteleiro Norte(SHN), Quadra 2, Bloco O
    Brasília, Brazil
    Monumental Bittar
    Setor Hoteleiro Norte(SHN), Quadra 3, Bloco B
    Postcode: 70702-912, Brasília, Brazil.
    El Pilar
    Setor Hoteleiro Norte(SHN), Quadra 3, Bloco F
    Postcode: 70710-300, Brasília, Brazil.
    Hotel Casablanca
    Setor Hoteleiro Norte(SHN), Lote A
    Postcode: 70703-900, Brasília, Brazil.

    These hotels are all within walking distance from each other.
    We will probably be able to provide transport from the hotel to the campus and back.

    Preliminary Program

    Monday, September 8, 2014.

    • 08:00-08:50 Registration
    • 08:50-09:00 Opening: Ian Mackie, M. Ayala-Rincón, Flávio de Moura, Daniele Nantes.
    • 9º Workshop on Logical and Semantic Frameworks, with Applications

    • 09:00-10:00 Invited Talk 1: Andrew Pitts - University of Cambridge

    • Constructive Type Theory with Abstractable Names

    • 10:00-10:30 Paulo Veloso, Sheila Veloso and Mario Benevides.
                  On Graph Calculi for Multi-modal Logics.
    • 10:30-11:00 Coffee-Break
    • 11:00-11:30 Jaime Árias, Michell Guzmán and Carlos Olarte.
                 A symbolic Model for Timed Concurrent Constraint Programming.
    • 11:30-12:00 Sandra Alves and Maribel Fernández.
               A Framework for the Analysis of Access Control Policies with Emergency Management.
    • 12:00-14:00 Lunch
    • 14:00-15:00 Invited Talk 2: Ugo Montanari - Università di Pisa

    • Network Conscious Pi-Calculus- A Model of Pastry

    • 15:00-15:30 Cláudia Nalon, Bruno Lopes, Gilles Dowek and Edward Hermann Haeusler
                A Calculus for Automatic Verification of Petri Nets based on Resolution and Dynamic Logics.
    • 15:30-16:00 Carlos Olarte and Elaine Pimentel.
                Proving Concurrent Constraint Programming Correct, Revisited.
    • 16:00-16:30 Coffee-Break
    • 16:30-17:00 Abeer Al-Humaimeedy and Maribel Fernández.
                Enabling Synchronous and Asynchronous Communications in CSP for SOC.
    • 17:00-17:20 Flávio L. C. De Moura.
                Higher-Order Unification via Explicit Substitutions at a Distance.
    • 17:20-17:40 Mario Piazza and Gabriele Pulcini.
                A Uniform Setting for Classical, Non-Monotonic and Paraconsistent Logic.
    • 20:00 Social Event (TBC)

    Tuesday, September 9, 2014

    • 09:00-10:00 Invited Talk 3: René Thiemann - Universität Innsbruck

    • A Framework for Developing Stand-Alone Certifiers

    • 10:00-10:30 Vincent Rahli, John Pirie, Joe Wells and Fairouz Kamareddine.
                Skalpel: A Type Error Slicer for Standard ML.
    • 10:30-11:00 Coffee-Break
    • 11:00-11:30 Alvaro Tasistro, Ernesto Copello and Nora Szasz.
                 Formalisation of Stoughton's Substitution for Lambda Calculus in Constructive Type Theory.
    • 11:30-12:00 Giuseppe Primiero.
                Intuitionistic Logic of Proofs with dependent proof terms.
    • 12:00-14:00 Lunch
    • Natural Deduction
    • 14:00-14:20 Marcus Ramos and Ruy De Queiroz.
                Formalization of Closure Properties for Context-Free Grammars.
    • 14:20-14:40 Cecilia Englander, Gilles Dowek and Edward Hermann Haeusler.
                 Yet Another Bijection Between Sequent Calculus and Natural Deduction.
    • 14:40-15:00 Natalia Novak.
                 Practical Extraction of Evidence Terms from Common-Knowledge Reasoning.
    • 15:00-15:20 Valeria de Paiva and Vivek Nigam.
               Towards a Rewriting Framework for Textual Entailment.
    • 15:20-16:00 LSFA Business Meeting
    • 16:00-16:30 Closing Coffee-Break


    In this ninth edition, the workshop will be held in September 8-9 at the Finatec located in University of Brasília.


    Finatec- Fundação de Empreendimentos Científicos e Tecnológicos
    Campus Universitário Darcy Ribeiro
    Av. L3 Norte, Ed. Finatec
    Asa Norte, Brasília – DF
    CEP 70910-900
    Tel.: +55 61 3348 0400

    Ver mapa maior

    Universidade de Brasília - Map




    Grupo de Teoria da Computação
    Departments of Mathematics and Computer Science
    Universidade de Brasília