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.

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.

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.

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)

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

lsfa2014@easychair.org
Home page: http://lsfa2014.cic.unb.br