headers
Sylvain Pogodalla | 8 Feb 2008 10:56
Picon
Favicon

[CFP] Workshop on Symmetric calculi and Ludics for the semantic interpretation

[Apologies for multiple postings]

SECOND CALL FOR PAPERS Workshop on Symmetric calculi and Ludics for
  the semantic interpretation
  (http://iml.univ-mrs.fr/~quatrini/ESSLLI2008.html) August 4-8, 2008

organized as part of the European Summer School on Logic, Language and
Information ESSLLI 2008 (http://www.illc.uva.nl/ESSLLI2008/), 4-15
August, 2008 in Hamburg, Germany

Workshop Organizers:

Alain Lecomte (SFL - Paris 8),  Alain.Lecomte@...
Myriam Quatrini (IML Marseille), quatrini@...

Workshop Purpose and topics:

  In recent years there have been some important new developments of
methods of dealing with semantic and pragmatic phenomena in
Linguistics, inspired by developments in Logic and Theoretical
Computer Science. Among these developments, Continuation Theory,
Symmetric calculi and Ludics play an important role. Continuation
theory dates back from the early seventies (cf. Reynolds, 93) and was
at the heart of Programming Languages like Scheme. More recently, a
logical account was given to it, by extending the Curry-Howard
homomorphism (Griffin, 1990),. This led to several calculi like such
as Parigot's lambda-mu-calculus, Curien-Herbelin's
lambda-mu-mu-tilde-calculus, Wadler's dual calculus and so on. These
calculi are based on the core idea that programs and contexts are dual
entities and this is reflected in the symmetry of the "classical"
(Continue reading)

Permalink | Reply | 0 comments |
headers
Elaine Pimentel | 18 Feb 2008 15:31
Picon
Gravatar

LSFA 2008 - First call for papers

     LSFA'08 - Third Workshop on Logical and Semantic Frameworks, with Applications
                                          August 26th, 2008
                                        Salvador, Bahia, Brazil

SCOPE

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 one-day workshop is to put together theoreticians
and practitioners to promote new techniques and results, from the
theoretical side, and feedback on the implementation and use of such
techniques and results, from the practical side.

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

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

LSFA'08 also aims to be a forum for presenting and discussing work in
progress, and therefore to provide feedback to authors on their
preliminary research. Submissions to the workshop will in the form of
full papers. The proceedings are produced only after the meeting, so
that authors can incorporate this feedback in the published papers.

INVITED SPEAKERS

César Muñoz NIA-NASA (Hampton)
02  (TBC)
03  (TBC)


PROGRAM COMMITTEE

Mauricio Ayala-Rincón UnB (Brasília)
Clemens Ballarin TUM (München)
Mario Benevides UFRJ (Rio de Janeiro), co-chair
Eduardo Bonelli UNQ (Quilmes)
Marcelo Coniglio UNICAMP (Campinas)
David Deharbe UFRN (Natal)
Clare Dixon University of Liverpool (Liverpool)
Gilles Dowek INRIA/École Polytechnique (Paris)
Marcelo Finger USP (São Paulo)
Bernhard Gramlich TU Wien (Vienna)
Edward Hermann Haeusler PUC-Rio (Rio de Janeiro)
Fairouz Kamareddine Heriot-Watt (Edinburgh)
Delia Kesner Paris 7 (Paris)
Claude Kirchner INRIA (Bordeaux)
Steffen Lewitzka UFBA (Salvador)
João Marcos UFRN (Natal)
Ana Teresa de Castro Martins UFC (Fortaleza)
Dale Miller INRIA/École Polytechnique (Paris)
Pierre-Etienne Moreau INRIA (Nancy)
Peter Mosses Swansea University (Swansea)
Anjolina Grisi de Oliveira UFPE (Recife)
Luca Paolini Università di Torino (Torino)
Elaine Pimentel UFMG (Belo Horizonte), co-chair
Simona Ronchi Della Rocca Università di Torino (Torino)
Alwen Tiu Australian National University
Yde Venema University of Amsterdam
Hongwei Xi Boston University (Boston)


ORGANIZING COMMITTEE

Mauricio Ayala-Rincón UnB (Brasília)
Edward Hermann Hauesler PUC-Rio (Rio de Janeiro)
Andreas Bernhard Michael Brunne UFBA (Salvador) Local-chair
Aline Maria Santos Andrade UFBA (Salvador) Local-chair


IMPORTANT DATES

Paper submission deadline:    May 18th
Author notification:               June 30th
Camera ready:                     July 20th


SUBMISSION INFORMATION

Contributions should be written in English and submitted in the form
full papers with at most 16 pages. They must be unpublished and not
submitted simultaneously for publication elsewhere. The submission
should be in the form of a PDF file uploaded to LSFA'08 page at
EasyChair until the submission deadline in May 18, by midnight, Central
European Standard Time (GMT+1).

The papers should be prepared in latex using Elsevier ENTCS style. The
workshop pre-proceedings, containing the reviewed extended abstracts,
will be handed-out at workshop registration and the proceedings will be
published as a volume of ENTCS.

After the workshop, according to the quantity and quality of selected papers,
the authors will be invited to submit full versions of their works that will be also
reviewed to high standards. A special issue of LSFA'06 appeared in the Journal of
Algorithms and currently a special issue of LSFA'07 is being processed and will
appear in The Logical Journal of the IGPL.

At least one of the authors should register at the conference. The
paper presentation should be in English.


CONTACT

Elaine Pimentel
elaine-Z7fn92kGNEcIdKJ7tpkyPg@public.gmane.org


Mario Benevides
mario-J2hdbf8UT7gIdKJ7tpkyPg@public.gmane.org


The web page of the event can be reached at:

http://www.mat.ufmg.br/lsfa2008
Permalink | Reply | 0 comments |
headers
Alessio Guglielmi | 25 Feb 2008 11:38
Picon
Favicon

Atomic flows

Hello,

Tom and I rewrote the paper on atomic flows, which has been accepted by LMCS.

Please, throw away the old version of that paper. 
There were no mistakes, but, thanks to the 
referees and those who read the old paper, 
especially Michel, this new version is much 
simpler and much better in almost every aspect. 
The only exception is that there is now a 
definition of atomic flow.

We plan to follow up this paper with another one 
where we will explore in much more detail the 
global transformations based on atomic flows. In 
particular, we obtain very simple cut elimination 
and interpolation procedures, and the 
streamlining procedure will be much more tightly 
determined by the topological structure of atomic 
flows.

I am now convinced of the truth and usefulness of the following slogan:

    bureaucracy-free proof system =
    CoS with inference rules on derivations =
    Formalism B =
    atomic flows + logical relations.

So, I think that atomic flows give us yet another 
perspective on which to base the design of a 
bureaucracy-free proof system of lasting value.

Please, keep the comments coming.

Ciao,

-Alessio

Normalisation Control in Deep Inference via Atomic Flows
Alessio Guglielmi and Tom Gundersen

We introduce `atomic flows´: they are graphs 
obtained from derivations by tracing atom 
occurrences and forgetting the logical structure. 
We study simple manipulations of atomic flows 
that correspond to complex reductions on 
derivations. This allows us to prove, for 
propositional logic, a new and very general 
normalisation theorem, which contains cut 
elimination as a special case. We operate in deep 
inference, which is more general than other 
syntactic paradigms, and where normalisation is 
more difficult to control. We argue that atomic 
flows are a significant technical advance for 
normalisation theory, because 1) the technique 
they support is largely independent of syntax; 2) 
indeed, it is largely independent of logical 
inference rules; 3) they constitute a powerful 
geometric formalism, which is more intuitive than 
syntax.

<http://cs.bath.ac.uk/ag/p/NormContrDIAtFl.pdf>
Permalink | Reply | 0 comments |

Gmane