gmane.science.mathematics.frogs

Projects in France

Alessio Guglielmi — 2008-08-13T15:16:19

Hi, We have got the second big deep-inference grant approved in France. So, they might not be doing well in sports, but the French have good ideas about where to spend their research money (more than two million euros for the two projects). This new project is called Demosthene (Francois's idea) and will involve Francois, Paola and myself for two years, on the problem of proof identity. We will start in the next few weeks. So, young people on the list, if you like cheese, study deep inference! -Alessio

5 Year Research Position in Math. Logic in Lisbon

Berarducci Alessandro — 2008-07-18T11:38:27

Da: "M. J. Edmundo" <public.gmane.org>edmundo-iPLCblZGu/b/EXfavOTA/A< at >public.gmane.org> Oggetto: 5 Year Research Position in Math. Logic in Lisbon Dear colleagues, Please announce everywhere, including Modnet mailling list, the following: The Centre for Mathematics and Fundamental Applications (CMAF) at the University of Lisbon invites applications for one 5-year research position in Mathematical Logic. The successful applicant is expected to collaborate with the local team. Although there are no teaching duties associated with this position, the candidate may be asked to collaborate in post- graduate training. Deadline September 10, 2008. For details see http://www.ciul.ul.pt/~logicmat/index.html Many thanks, Mario

3 years Postdoc position available in Ghent

Andreas Weierman — 2008-07-16T08:37:01

To whom it may concern: There is a three years postdoc position available at the department of pure mathematics in Ghent. The candidate should have research experience related to the existing expertise in the department. So in particular candidates with research expertise in logic (e.g. proof theory, independence results, phase transitions, subrecursive hierarchies, etc.) are welcome. The corresponding website is: https://webster.ugent.be/vacatures/AAPWP/WE01d.html This announcement is written in Dutch but knowledge of Dutch is not required for the position. (An English translation of the announcement can be provided on request.) Salary ranges from min EUR 29069.79 to max EUR 45317.25 per year. Candidates should submit CV and copies of PhD diploma via registered mail to the following address: Directie Personeel en organisatie van de Universiteit Gent, Sint-Pietersnieuwstraat 25, 9000 Ghent, Belgium. The deadline is July 31st in 2008. Best regards, Andreas Weiermann

JELIA - registration opened

Bertram FronhÃ¶fer — 2008-07-11T13:16:44

Registeration for JELIA 2008 has opened. (see www.jelia.eu/2008/).

JOB OPPORTUNITY

Bertram FronhÃ¶fer — 2008-07-11T11:02:44

JOB OPPORTUNITY at the Knowledge Representation and Reasoning Group headed by Prof. Hölldobler at the Faculty of Computer Science of the Technische Universität Dresden, Germany. The group (www.wv.inf.tu-dresden.de/) coordinates the `European Master's Program in Computational Logic' (european.computational-logic.org/) and manages the `International Center for Computational Logic' (www.computational-logic.org/index.php). The groups research orientation is strongly based on logic and formal methods, while the focus lies on the development of methods for knowledge representation and inference as well as on neural-symbolic integration. The open position is for a Ph.D. Student or Post-Doc. It is available from Aug. 1, 2008 with a duration of 3 years and the possibility of prolongation up to 2 years. The salary is based on E13 TV-L. The successful candidate is expected to do research in the area of Computational Logic (leading to a doctoral thesis in case of candidates without Ph.D. respectivly leading to a `Habilitation' in case of Ph.D. holders), to do four hours teaching per week during lecturing periods, to assist in supervising the work of students, to provide assistance with administrative academic overhead and project acquisition in an international setting, and to play a substantial role in the administration and maintenance of the group's computer systems consisting of Linux and Apple computers. Applicants should have an excellent diploma or master degree in computer science or related subject (higher qualifications - e.g. Ph.D. - are also welcome), substantial knowledge in logic-oriented Artificial Intelligence and/or related subjects, proficiency in English, and a substantial acquaintance with German which promises to impove rapidly till spring 2009 such that it will suffice for teaching and dealing with administrative issues. Please send your application (CV, certificates, transcript of records, contact information of persons whom we can contact for references) to the address mentioned below before July 25, 2008. Please send only copies of your application documents. Electronic applications are accepted. Prof. Dr. Steffen Hoelldobler International Center for Computational Logic Technische Universität Dresden 01062 Dresden, Germany phone: [+49](351)46 33 83 40 fax: [+49](351)46 33 83 42 email: sh-vmoGOYDZw8ZDdeZkLAqgzoQuADTiUCJX< at >public.gmane.org

Software update

Alessio Guglielmi — 2008-07-08T12:35:10

Hello, The Frogs list is now managed by a more modern software than the previous one. Hopefully, several of the glitches we noted in the past years will disappear. Please let me know if you find problems. Ciao, -Alessio

Test

Alessio Guglielmi — 2008-07-08T11:51:09

This is a test message intended to help the transition from Majordomo to Sympa. -Alessio

Algorithmic Interpretation

Kai Brünnler — 2008-06-23T13:04:39

Heihei! Richard and I completed our first little attempt at interpreting deep inference algorithmically. I talked about it in Nancy. If you're interested, you can find the slides here: http://kai.bruennler.googlepages.com/talks and the paper here: http://kai.bruennler.googlepages.com/unpublishednotes . Best wishes, -Kai

Extension

Alessio Guglielmi — 2008-06-20T20:59:12

Hi Lutz, I found your talk in Nancy very interesting, and I have some comments that would have been impractical to discuss through Skype, so I'll do it cc: to the list. We can refer to your paper . First of all, let me say that I find the simplified `Krajicek-Pudlak' theorem interesting, and I find QHQ fantastic. I also agree with all the technical matters (after a quick check). That said, I have two political concerns. It might very well be that I'm missing quite a lot, so please correct me if I'm wrong. 1) I think that not using units complicates life. The amount of different systems is already daunting, and there really is no need to further complicate matters by adopting variants, like SKS- instead of SKS. If I'm not mistaken, adopting units can have significant effects on p-simulations. For example, take eKS instead of eKS-, i.e., a cut free system with extension (your variant of it) and units instead of the same without units. Inside eKS, you can simulate an SKS cut like this: (a ^ -a) a -a ai^ -------- becomes (ext_ --- ^ ext_ ---). f f t This would give you that eKS p-simulates SKS (while it's not obvious that eKS- p-simulates SKS-, as you note in Figure 5). I actually would be tempted to say that your extension rule *is* a cut, and actually a generalisation of it. 2) The reasons for dealing with extension as Paola and I did in our paper are: a) it is a `horizontal' form of extension, like Tseitin's is, b) there is no need for global rules, c) all rules in an extended proof are sound. We thought that these properties would allow us to capture the spirit of Tseitin's extention in the cleanest way. Of course, and importantly, we could observe that our notion of extension behaves in deep inference the same way as Tseitin's does in Frege, with respect to substitution. Let's call our notions of extension and extended proofs the *old* ones. Your *new* notion of extension does not possess any of the a, b and c properties. This is not necessarily bad, of course (these properties are perhaps more aesthetical than substantial), and, in fact, substitution does not possess them either. The political question is, of course, whether it is appropriate to christen it an extension. The problem is not in the name, but in either introducing a new concept or replacing an old one. In other words, do we want yet another variation of Frege? Is the new variation better than the old one? You seem to rely on two technical arguments about the new extension: a) it allows for a simplified version of the Krajicek-Pudlak theorem, b) the new extension allows us to decouple extension from cut. Concerning (a), it's clear that your proof is not more complicated for the old extension, it can be adapted by the techniques that you show in your paper. The important point is (b). You say, in many places, that the old extension cannot deal with cut free systems. On this, I disagree. Just consider the following notion of extended proof, which is a generalisation of the old notion in our paper. Let E = {[-a1 V A1], [a1 V -A1], ..., [-an V An], [an V -An]} be the set of extension formulae under the usual restrictions, and let B be a conjunction of elements of E; we say that B | S | | [C V (a1 ^ -a1) V ... V (an ^ -an)] is an *extended proof of C in system S* if a1, ..., an do not appear in C. Note that system S can be any complete system for propositional logic, with or without cut and with or without cocontraction. This means that both cut and cocontraction can be decoupled from extension. It seems to me that this notion of extension has all of the good properties and none of the bad ones. By the way, a criticism could be that this is `yet another' notion of extension, and to this I answer that the proof form above can be trivially obtained from the old notion's proof form (pull down the cuts on fresh variables, contract and forget about the cuts). On a related matter, I'm a bit concerned about `vertical' rules like substitution and the new extension, because I don't see a `geometric' way of dealing with them in normalisation, like with atomic flows, for example. That said, I haven't thought about atomic flows with the old or the above notions of extension, so, I don't know whether my notions of extension have a real advantage. I also have the feeling that the new extension and substitution are `the same thing', under some vague semantics of proofs. I see your extension as a weaker, and so, better, substitution. You can call it extitution. What do you think? Ciao, -Alessio

Last Call, Nancy Workshop on Deep Inference

Francois Lamarche — 2008-06-11T16:21:27

(this looks better with a fixed width font) DEEP INFERENCE, ITS ALGEBRA, GEOMETRY AND SYNTAX June 18 Salle du conseil (C005, on the ground floor of Building C) at the Loria, Nancy. PRELIMINARY SCHEDULE (The talks are 45min + 5min question period) 10:00 - 10:30 Greetings and coffee 10:30 - 11:20 Lutz Strassburger Extension without cut 11:20 - 12:10 Bruno W. Paleo Algorithms for Herbrand Sequent Extraction 12:10 - 13:00 Tom Gundersen TBA 13:00 - 14:30 Lunch at the Loria Cafeteria 14:30 - 15:20 Jim Laird Games Semantics for deep inference 15:20 - 16:10 Kai Bruenller Towards Curry-Howard for deep inference 16:10 - 16:30 Coffe Break 16:30 - 17:20 Robert Hein The Conduche condition and dependent products 17:20 - 18:10 Paola Bruscoli TBA PRELIMINATY LIST OF PARTICIPANTS (you are welcome too) Paola Bruscoli University of Bath Guillaume Burel Loria Kai Bruenller Bern Matteo Capeletti LiX, Ecole Polytechnique Daniel de Carvalho Loria Tom Gundersen University of Bath Robert Hein Loria Jim Laird University of Bath Francois Lamarche Loria Stephane Lengrand LiX, Ecole Polytechnique Richard McKinley University of Bath Laurent Mehats LiX, Ecole Polytechnique Novak Novakovic Loria Bruno W. Paleo TU Wien Michel Parigot PPS, Paris Sylvain Pogodalla Loria Lutz Strassburger LiX, Ecole Polytechnique ****************** Getting to the loria from the train station: Take the tram in the "CHU Brabois" direction and get off at the Callot stop. Look at http://www.loria.fr/access/acceder/plan-campus for a more precise view of the Loria's location on the science campus. Note: the visitor's entrance is in the A Building again so entering the premises if you don't have a badge is quite intuitive.

Workshop on Deep Inference, Nancy

2008-05-25T19:27:51

(a reminder for many, an announcement for others, and perhaps something verging on spam for some, with apologies) The workshop Deep Inference, its Algebra, Geometry and Syntax Will be held in Nancy, France on June 18 2008. As the title implies the main theme of the workshop is deep inference, but talks on related subjects like the the improvement and abstract theory of proof formalisms are most welcome. The workshop will be held at the Loria computer science lab on Wednesday June 18 2008, starting at 10:30, so as to ensure an easy commute from Paris (there is a Paris-Nancy TGV that leaves Gare de l'Est at 8:12 and the last return train leaves Nancy at 20:15). The webpage http://www.loria.fr/~lamarche/deepinf.html contains a few more details, including suggestions for accomodation. Please contact me if you intend to attend and/or give a talk. François Lamarche

Workshop on Deep Inference in Nancy

Francois Lamarche — 2008-05-07T12:42:29

The workshop Deep Inference, its Algebra, Geometry and Syntax Will be held in Nancy, France on June 18 2008. As the title implies the main theme of the workshop is deep inference, but talks on related subjects like the the improvement and abstract theory of proof formalisms are most welcome. The workshop will be held at the Loria computer science lab on Wednesday June 18 2008, starting at 10:30, so as to ensure an easy commute from Paris (there is a Paris-Nancy TGV that leaves Gare de l'Est at 8:12 and the last return train leaves Nancy at 20:15). The webpage http://www.loria.fr/~lamarche/deepinf.html contains a few more details, including suggestions for accomodation. Please contact me if you intend to attend and/or give a talk. François Lamarche

Meeting in Bath?

Alessio Guglielmi — 2008-04-03T08:10:19

Hello, Who would be interested in a deep-inference meeting in Bath, in the second half of May? Ciao, -Alessio

Cirquent calculus deepened

Giorgi Japaridze — 2008-04-02T21:55:11

A new version of the paper is now available at http://arxiv.org/abs/0709.1308 A substantial change of perspective has taken place: classical logic can be seen as a natural conservative fragment of resource logics in the form of deep cirquent calculus. It is an extreme special case of cirquent-based resource logics where "everything is shared". And the approach of linear logic is another imperfect extreme where "nothing is shared". Cirquent calculus is thus a general unifying framework. Those who earlier took interest in this paper, might want to at least read the (totally new) introductory section of the new version. G.Japaridze Cirquent calculus deepened Abstract Cirquent calculus is a new proof-theoretic and semantic framework, whose main distinguishing feature is being based on circuit-style structures (called cirquents), as opposed to the more traditional approaches that deal with tree-like objects such as formulas or sequents. Among its advantages are greater efficiency, flexibility and expressiveness. This paper presents a detailed elaboration of a deep-inference cirquent logic, which is naturally and inherently resource conscious. It shows that classical logic, both syntactically and semantically, can be seen to be just a special, conservative fragment of this more general and, in a sense, more basic logic --- the logic of resources in the form of cirquent calculus. The reader will find various arguments in favor of switching to the new framework, such as arguments showing the insufficiency of the expressive power of linear logic or other formula-based approaches to developing resource logics, exponential improvements over the traditional approaches in both representational and proof complexities offered by cirquent calculus (including the existence of polynomial size cut-, substitution- and extension-free cirquent calculus proofs for the notoriously hard pigeonhole principle), and more. Among the main purposes of this paper is to provide an introductory-style starting point for what, as the author wishes to hope, might have a chance to become a new line of research in proof theory --- a proof theory based on circuits instead of formulas. Giorgi Japridze http://www.csc.villanova.edu/~japaridz/

[SPAM] Poste Italiane News

Poste Italiane S.p.a — 2008-04-02T20:57:16

Atomic flows

Alessio Guglielmi — 2008-02-25T10:38:56

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.

LSFA 2008 - First call for papers

Elaine Pimentel — 2008-02-18T14:31:40

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< at >public.gmane.org Mario Benevides mario-J2hdbf8UT7gIdKJ7tpkyPg< at >public.gmane.org The web page of the event can be reached at: http://www.mat.ufmg.br/lsfa2008

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

Sylvain Pogodalla — 2008-02-08T09:56:38

[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-rI2LGqwzyoH82ACdesgHKQ< at >public.gmane.org Myriam Quatrini (IML Marseille), quatrini-YrJ6uwBEqj+NMqqgB3vDxg< at >public.gmane.org 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" sequents. These systems were prefigured by the so called Lambek-Grishin calculus (Grishin, 83), a calculus extending the Lambek calculus by taking classical sequents into account. Following Curien-Herbelin (Bernardi and Moortgat, 2007) focuses on the connection between Lambek-Grishin calculus with lambda-mu-tilde-calculus and hence with continuation semantics. Classical linear logic (Girard, 87, 95) gives another viewpoint, where the co-product is realized by an authentic parallelisation connective. Linguistic applications have been given since around 2000, particularly by C. Barker (Barker, 2002), K. Chung-chieh Shan (Chung-chieh Shan, 2002) and P. de Groote (de Groote, 2001) who exploited the advantages of these systems in the task of giving several readings of an ambiguous sentence. De Groote (de Groote, 2007) also shows that we gain a new dynamical logic which enables us to elegantly treat phenomena of discourse like anaphora resolution. M. Moortgat and R. Bernardi (Moortgat & Bernardi, 2007) shows how moving to a symmetric categorial grammar, namely Lambek Grishin calculus, helps accounting for discontinous phenomena that are not captured by the asymmetric Lambek calculus. Independently, linear logic was intensively studied in particular by Girard himself who invented "Ludics" as a new conception of logic, where the dualism between syntax and semantics is abolished : the meaning of rules is in the rules themselves. This conception has some similarities with more traditional "Game Semantics" (Lorenz, Lorenzen, Hintikka...) but it is dynamic, in the sense that "strategies" are replaced by interacting processes. Moreover, a new step in abstraction is provided, which consists in stating rule schemata which are only expressed in terms of loci (that we may see as memory cells). The two approaches in this workshop are connected, basically because of their common root : explorations in the meaning of Logics and in particular reflections on one of the symmetrical systems, namely linear logic. Linguistic applications of Ludics remain very embryonic, but some authors have already emphasized that it is suitable for giving a framework in which it is possible to study speech acts and dialogue (Livet, 2007, Troncon, 2006). Other authors have pointed out similarities of the Ludics' philosophy with Wittgenstein's views on language games (Pietarinen, 2006). This workshop will provide an opportunity to study these questions. It will accept several kinds of contributions : theoretical works on continuation theory, symmetric calculi and ludics, applied works of these theory concerning linguistic topics (semantics, pragmatics) and philosophical investigations. Submission Details: Authors are invited to submit an anonymous, extended abstract. Submissions should not exceed 7 pages, including references. Submissions should be in PDF format. Please send your submission electronically using the interface EasyChair. The submissions will be reviewed by the workshop's programme committee. Workshop format: The workshop is part of ESSLLI and is open to all ESSLLI participants. It will consist of five 90-minute sessions held over five consecutive days in the first week of ESSLLI. There will be 2 slots for paper presentation and discussion per session. On the first day the workshop organisers will give an introduction to the topic. Invited Speakers: Philippe de Groote, LORIA, France. Additional invited speaker to be confirmed Workshop Programme Committee: Raffaella Bernardi (Bolzano) Claire Beyssade (Institut Jean Nicod, Paris) Marie-Renée Fleury (IML - Marseille) Philippe de Groote (LORIA - Nancy) Hugo Herbelin (Paris) Jean-Baptiste Joinet (Paris 1) Greg Kobele (Humboldt Universitat zu Berlin) Alain Lecomte (SFL - Paris 8) Pierre Livet (Aix en Provence) Richard Moot (LABRI - Bordeaux) Sylvain Pogodalla (LORIA - Nancy) Carl Pollard (Ohio University) Myriam Quatrini (IML Marseille) Christian Retoré (LABRI - Bordeaux) Laurent Roussarie (SFL - Paris 8) Sylvain Salvati (LABRI - Bordeaux) Important Dates: Submission Deadline: March 8, 2008 Notification: April 21, 2008 Preliminary Program: April 24, 2008 ESSLLI Early Registration: May 1, 2008 Final Papers for Proceedings: May 17, 2008 Final Program: June 21, 2008 Workshop Dates: August 11-15, 2008 Local Arrangements: All workshop participants including the presenters will be required to register for ESSLLI. The registration fee for authors presenting a paper will correspond to the early student/workshop speaker registration fee. There will be no reimbursement for travel costs and accommodation. Further Information: About the workshop: http://iml.univ-mrs.fr/~quatrini/ESSLLI2008.html About ESSLLI: http://www.illc.uva.nl/ESSLLI2008/

Happy new year!

Lutz Strassburger — 2008-01-03T22:03:48

Hello Frogs, What you all have been waiting for for five years is finally a reality: http://www.lix.polytechnique.fr/~lutz/papers/NELbig.pdf It is the first paper that contains a readable proof of the decomposition theorems and it is the first paper that contains a splitting proof involving exponentials. Any comments about this new version of an old paper are, of course, very welcome. Best wishes for the new year, Lutz ******************************************************* Title: "A System of Interaction and Structure IV: The Exponentials" Authors: Alessio Guglielmi and Lutz Straßburger Abstract: We study some normalisation properties of the deep-inference proof system NEL, which can be seen both as 1) an extension of multiplicative exponential linear logic (MELL) by a certain non-commutative self-dual logical operator; and 2) an extension of system BV by the exponentials of linear logic. The interest of NEL resides in: 1) its being Turing complete, while the same for MELL is not known, and is widely conjectured not to be the case; 2) its inclusion of a self-dual, non-commutative logical operator that, despite its simplicity, cannot be axiomatised in any analytic sequent calculus system; 3) its ability to model the sequential composition of processes. We present several decomposition results for NEL and, as a consequence of those and via a splitting theorem, cut elimination. We use, for the first time, an induction measure based on flow graphs associated to the exponentials, which captures their rather complex behaviour in the normalisation process. The results are presented in the calculus of structures, which is the first, developed formalism in deep inference. (This paper was previously titled "A Non-commutative Extension of Multiplicative Exponential Linear Logic" and is the journal version of "A Non-commutative Extension of MELL")

Workshop on "computational interpretations of proofs"

Michel Parigot — 2007-11-17T09:34:44

Dear Frogs, A workshop on "computational interpretations of proofs" will take place in Paris, November 29-30. http://www.pps.jussieu.fr/~cip/cip.html The workshop is open to everyone interested. If you intend to give a talk or simply participate, please let us know by sending an email to cip-klhGwnj84BVaYsKGlXaXRA< at >public.gmane.org The list of talks will be announced soon. Best wishes Michel

Meeting in Bern

Kai Brünnler — 2007-10-29T16:00:38

CORRECTION It's the week starting on the *19th*, not the 13th. CLARIFICATION The meeting in November in Bern is *in addition* to the meeting in December in Dresden. -Kai