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.
- Submission: Sunday
25th May 8th June (extended deadline)
Friday 11th July Monday 21st July (New!)
- Preliminary proceedings version due: Sunday 3rd August
- Submission for final proceedings: Sunday 19th October
- Notification: Friday 28th November
- Final version: Sunday 21st December
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 (University of 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
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)
Home page: http://lsfa2014.cic.unb.br
At least one of the authors of accepted papers should register at the conference.
Early registration (payment until August 25th, 2014)
R$ 220,00 or U$100,00
R$ 330,00 or U$150,00
Late registration (payment from August 26th, 2014 on)
R$260,00 or U$ 120,00
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 may pay in cash on the arrival at the meeting.
Banco do Brasil
Nome: Daniele Nantes Sobrinho
, please send an email to
with the following
- Date of Arrival/Departure
- Copy of the bank deposit
We will confirm the registration within 3 days.