gmane.science.mathematics.frogs

Last CFP: Workshop on Logics for Resources, Processes and Programs (LRPP 2012)

Pym, Professor David J. — 2012-05-08T17:30:47

------------------------------------------------------------------------------
Call For Papers

Workshop on Logics for Resources, Processes and Programs
(LRPP 2012)

1st July 2012, Manchester, UK

(affiliated with IJCAR 2012, Manchester, UK)

http://www.loria.fr/~galmiche/LRPP2012.html

Extended deadline: May 20, 2012
----------------------------------------------------------------------

A one day workshop on `Logics for Resources, Processes, and Programs'
will be held the 1st July 2012 in conjunction with the IJCAR 2012
Conference in Manchester, UK, with D. Galmiche and D. Pym as organizers.

The purpose of this workshop would be to discuss recent results on
logics, including systems formulated in the style of Hoare and
Hennessy-Milner, for modelling resources, processes, programs, and
their interactions. We envisage a range of perspectives:
proof-theoretic foundations, including decidability and complexity;
semantic foundations (e.g., new resource semantics); specification of
properties and behaviours; verification and analysis of programs and
systems. It should help to establish and publicize a research agenda
for such logics and their use in the development of trusted
systems.

The workshop is intended to provide a forum for discussion between
researchers interested in logics of resources (from foundations to
related calculi and applications) and researchers interested in
languages and methods for specification of mobile, distributed,
concurrent systems and their verification.


Topics of interest include, but are not restricted to,
the following:

- Logics for resources: semantics and proof theory;
- Process calculi, concurrency, resource-distribution;
- Reasoning about programs and systems;
- Extensions of logics; e.g., with modalities;
- Languages of assertions, languages based on resource logics (query
  languages, pointers, trees, and graphs) and reasoning;
- Theorem proving and model checking in resource logics:
  decision procedures, strategies, complexity results.

KEYNOTE SPEAKER

Peter O'Hearn (UCL, London,UK)

SUBMISSIONS

Researchers interested in presenting their works are invited to send an
extended abstract (up to 10 pages) by e-mail submissions of PDF files
to D. Galmiche (Didier.Galmiche-/zGXu1G9BXs< at >public.gmane.org) and D. Pym
(d.j.pym-9qr1vRpWqPK1Qrn1Bg8BZw< at >public.gmane.org) by May 20th 2012.

Papers will be reviewed by peers, typically members of
the Programme Committee.

Additional information will be available through WWW address:
http://www.loria.fr/~galmiche/LRPP2012.html.

Hardcopies of the preliminary proceedings will be distributed at the
workshop and a Special Issue of a Journal on these topics is expected
after the workshop.

PROGRAM COMMITTEE

J. Brotherston (Queen Mary, London, UK)
M. Collinson (University of Aberdeen, Scotland)
D. Galmiche (LORIA, Nancy, France: Co-chair)
J. Harland (RMIT University, Melbourne, Australia)
M. Hennessy (Trinity College, Dublin, Ireland)
D. Larchey-Wendling (LORIA, Nancy, France)
F. Pfenning (CMU, Pittsburgh, USA)
D. Pym (University of Aberdeen, Scotland: Co-chair)


IMPORTANT DATES

Submissions:  May 20, 2012
Notifications: May 30, 2012
Final papers: June 10, 2004

Workshop date: July 1st, 2012


MORE INFORMATION

E-mail: Didier.Galmiche-/zGXu1G9BXs< at >public.gmane.org and d.j.pym-9qr1vRpWqPK1Qrn1Bg8BZw< at >public.gmane.org






The University of Aberdeen is a charity registered in Scotland, No SC013683.

J N wants to be your friend on Windows Live

J N — 2012-01-08T09:32:56

J N wants to be your friend on Windows Live
<https://profile.live.com/cid-fee5726b043f694d/?invite=e8677e0929938eda2%3aFbCLGUsUfYVqKWK2lUMq6H6ZMFna1brAE60VXvYBmQfE%2bhCYxmqfyYfwEQtTa6V4BFxEed5PeieEWKwGvZMej21yKeb4PdtqhGZ6P4Rf27Zks%2ffXyTlYa1u56asMMxS%2b&ids=ChseM4InGnCmhXO%21WXdtt7%21LrheJ4zuyCEkIDX8OqJ%2ah%2auy6JYexgFQ2iB4oVSq4DJbEbZp62be056Q3UQaSEYihlh0%2aB0tA16BGj4sE6%214yLA51o6ikpm2d58fTC0dSWQqoHlfpqtCNe68YNAc40lrUl%21K5s42VZ%21sK5M0J3M0b&Bsrc=EMINGM&Bpub=SN.Notifications>
""
View invitation
<https://profile.live.com/cid-fee5726b043f694d/?invite=e8677e0929938eda2%3aFbCLGUsUfYVqKWK2lUMq6H6ZMFna1brAE60VXvYBmQfE%2bhCYxmqfyYfwEQtTa6V4BFxEed5PeieEWKwGvZMej21yKeb4PdtqhGZ6P4Rf27Zks%2ffXyTlYa1u56asMMxS%2b&ids=ChseM4InGnCmhXO%21WXdtt7%21LrheJ4zuyCEkIDX8OqJ%2ah%2auy6JYexgFQ2iB4oVSq4DJbEbZp62be056Q3UQaSEYihlh0%2aB0tA16BGj4sE6%214yLA51o6ikpm2d58fTC0dSWQqoHlfpqtCNe68YNAc40lrUl%21K5s42VZ%21sK5M0J3M0b&Bsrc=EMINGM&Bpub=SN.Notifications>
Notifications preferences
<https://profile.live.com/options/notifications/>
Microsoft privacy statement
<http://g.msn.com.ph/2privacy/ensg>
Microsoft Corporation, One Microsoft Way, Redmond, WA 98052

J N wants to be your friend on Windows Live

J N — 2012-01-08T09:27:40

J N wants to be your friend on Windows Live
<https://profile.live.com/cid-fee5726b043f694d/?invite=dffafc49b6d74ab42%3acTO%2frcTllE8ULIZ%2bbZ1lNl%2bQL8%2b4MgQLXL11%2bpAu9YyrI5ycqv8QTKCCTiP41lrs8HJpfihiBMVkXUedyDIbCfick2kVilRs456JOIJ0%2bbGxlHG2lAcO9mnb%2b0YUyk6C&ids=ChseM4InGnCmhXO%21WXdtt7%21LrheJ4zuyCEkIDX8OqJ%2ah%2auy6JYexgFQ2iB4oVSq4DJbEbZp62be056Q3UQaSEYihlh0%2aB0tA16BGj4sE6%214yLA51o6ikpm2d58fTC0dSWQqoHlfpqtCNe68YNAc40lrUl%21K5s42VZ%21sK5M0J3M0b&Bsrc=EMINGM&Bpub=SN.Notifications>
""
View invitation
<https://profile.live.com/cid-fee5726b043f694d/?invite=dffafc49b6d74ab42%3acTO%2frcTllE8ULIZ%2bbZ1lNl%2bQL8%2b4MgQLXL11%2bpAu9YyrI5ycqv8QTKCCTiP41lrs8HJpfihiBMVkXUedyDIbCfick2kVilRs456JOIJ0%2bbGxlHG2lAcO9mnb%2b0YUyk6C&ids=ChseM4InGnCmhXO%21WXdtt7%21LrheJ4zuyCEkIDX8OqJ%2ah%2auy6JYexgFQ2iB4oVSq4DJbEbZp62be056Q3UQaSEYihlh0%2aB0tA16BGj4sE6%214yLA51o6ikpm2d58fTC0dSWQqoHlfpqtCNe68YNAc40lrUl%21K5s42VZ%21sK5M0J3M0b&Bsrc=EMINGM&Bpub=SN.Notifications>
Notifications preferences
<https://profile.live.com/options/notifications/>
Microsoft privacy statement
<http://g.msn.com.ph/2privacy/ensg>
Microsoft Corporation, One Microsoft Way, Redmond, WA 98052

J N wants to be your friend on Windows Live

J N — 2012-01-08T09:32:56

J N wants to be your friend on Windows Live
<https://profile.live.com/cid-fee5726b043f694d/?invite=e8677e0929938eda2%3aFbCLGUsUfYVqKWK2lUMq6H6ZMFna1brAE60VXvYBmQfE%2bhCYxmqfyYfwEQtTa6V4BFxEed5PeieEWKwGvZMej21yKeb4PdtqhGZ6P4Rf27Zks%2ffXyTlYa1u56asMMxS%2b&ids=ChseM4InGnCmhXO%21WXdtt7%21LrheJ4zuyCEkIDX8OqJ%2ah%2auy6JYexgFQ2iB4oVSq4DJbEbZp62be056Q3UQaSEYihlh0%2aB0tA16BGj4sE6%214yLA51o6ikpm2d58fTC0dSWQqoHlfpqtCNe68YNAc40lrUl%21K5s42VZ%21sK5M0J3M0b&Bsrc=EMINGM&Bpub=SN.Notifications>
""
View invitation
<https://profile.live.com/cid-fee5726b043f694d/?invite=e8677e0929938eda2%3aFbCLGUsUfYVqKWK2lUMq6H6ZMFna1brAE60VXvYBmQfE%2bhCYxmqfyYfwEQtTa6V4BFxEed5PeieEWKwGvZMej21yKeb4PdtqhGZ6P4Rf27Zks%2ffXyTlYa1u56asMMxS%2b&ids=ChseM4InGnCmhXO%21WXdtt7%21LrheJ4zuyCEkIDX8OqJ%2ah%2auy6JYexgFQ2iB4oVSq4DJbEbZp62be056Q3UQaSEYihlh0%2aB0tA16BGj4sE6%214yLA51o6ikpm2d58fTC0dSWQqoHlfpqtCNe68YNAc40lrUl%21K5s42VZ%21sK5M0J3M0b&Bsrc=EMINGM&Bpub=SN.Notifications>
Notifications preferences
<https://profile.live.com/options/notifications/>
Microsoft privacy statement
<http://g.msn.com.ph/2privacy/ensg>
Microsoft Corporation, One Microsoft Way, Redmond, WA 98052

J N wants to be your friend on Windows Live

J N — 2012-01-08T09:27:40

J N wants to be your friend on Windows Live
<https://profile.live.com/cid-fee5726b043f694d/?invite=dffafc49b6d74ab42%3acTO%2frcTllE8ULIZ%2bbZ1lNl%2bQL8%2b4MgQLXL11%2bpAu9YyrI5ycqv8QTKCCTiP41lrs8HJpfihiBMVkXUedyDIbCfick2kVilRs456JOIJ0%2bbGxlHG2lAcO9mnb%2b0YUyk6C&ids=ChseM4InGnCmhXO%21WXdtt7%21LrheJ4zuyCEkIDX8OqJ%2ah%2auy6JYexgFQ2iB4oVSq4DJbEbZp62be056Q3UQaSEYihlh0%2aB0tA16BGj4sE6%214yLA51o6ikpm2d58fTC0dSWQqoHlfpqtCNe68YNAc40lrUl%21K5s42VZ%21sK5M0J3M0b&Bsrc=EMINGM&Bpub=SN.Notifications>
""
View invitation
<https://profile.live.com/cid-fee5726b043f694d/?invite=dffafc49b6d74ab42%3acTO%2frcTllE8ULIZ%2bbZ1lNl%2bQL8%2b4MgQLXL11%2bpAu9YyrI5ycqv8QTKCCTiP41lrs8HJpfihiBMVkXUedyDIbCfick2kVilRs456JOIJ0%2bbGxlHG2lAcO9mnb%2b0YUyk6C&ids=ChseM4InGnCmhXO%21WXdtt7%21LrheJ4zuyCEkIDX8OqJ%2ah%2auy6JYexgFQ2iB4oVSq4DJbEbZp62be056Q3UQaSEYihlh0%2aB0tA16BGj4sE6%214yLA51o6ikpm2d58fTC0dSWQqoHlfpqtCNe68YNAc40lrUl%21K5s42VZ%21sK5M0J3M0b&Bsrc=EMINGM&Bpub=SN.Notifications>
Notifications preferences
<https://profile.live.com/options/notifications/>
Microsoft privacy statement
<http://g.msn.com.ph/2privacy/ensg>
Microsoft Corporation, One Microsoft Way, Redmond, WA 98052

J N wants to be your friend on Windows Live

J N — 2012-01-08T09:32:56

J N wants to be your friend on Windows Live
<https://profile.live.com/cid-fee5726b043f694d/?invite=e8677e0929938eda2%3aFbCLGUsUfYVqKWK2lUMq6H6ZMFna1brAE60VXvYBmQfE%2bhCYxmqfyYfwEQtTa6V4BFxEed5PeieEWKwGvZMej21yKeb4PdtqhGZ6P4Rf27Zks%2ffXyTlYa1u56asMMxS%2b&ids=ChseM4InGnCmhXO%21WXdtt7%21LrheJ4zuyCEkIDX8OqJ%2ah%2auy6JYexgFQ2iB4oVSq4DJbEbZp62be056Q3UQaSEYihlh0%2aB0tA16BGj4sE6%214yLA51o6ikpm2d58fTC0dSWQqoHlfpqtCNe68YNAc40lrUl%21K5s42VZ%21sK5M0J3M0b&Bsrc=EMINGM&Bpub=SN.Notifications>
""
View invitation
<https://profile.live.com/cid-fee5726b043f694d/?invite=e8677e0929938eda2%3aFbCLGUsUfYVqKWK2lUMq6H6ZMFna1brAE60VXvYBmQfE%2bhCYxmqfyYfwEQtTa6V4BFxEed5PeieEWKwGvZMej21yKeb4PdtqhGZ6P4Rf27Zks%2ffXyTlYa1u56asMMxS%2b&ids=ChseM4InGnCmhXO%21WXdtt7%21LrheJ4zuyCEkIDX8OqJ%2ah%2auy6JYexgFQ2iB4oVSq4DJbEbZp62be056Q3UQaSEYihlh0%2aB0tA16BGj4sE6%214yLA51o6ikpm2d58fTC0dSWQqoHlfpqtCNe68YNAc40lrUl%21K5s42VZ%21sK5M0J3M0b&Bsrc=EMINGM&Bpub=SN.Notifications>
Notifications preferences
<https://profile.live.com/options/notifications/>
Microsoft privacy statement
<http://g.msn.com.ph/2privacy/ensg>
Microsoft Corporation, One Microsoft Way, Redmond, WA 98052

J N wants to be your friend on Windows Live

J N — 2012-01-08T09:27:40

J N wants to be your friend on Windows Live
<https://profile.live.com/cid-fee5726b043f694d/?invite=dffafc49b6d74ab42%3acTO%2frcTllE8ULIZ%2bbZ1lNl%2bQL8%2b4MgQLXL11%2bpAu9YyrI5ycqv8QTKCCTiP41lrs8HJpfihiBMVkXUedyDIbCfick2kVilRs456JOIJ0%2bbGxlHG2lAcO9mnb%2b0YUyk6C&ids=ChseM4InGnCmhXO%21WXdtt7%21LrheJ4zuyCEkIDX8OqJ%2ah%2auy6JYexgFQ2iB4oVSq4DJbEbZp62be056Q3UQaSEYihlh0%2aB0tA16BGj4sE6%214yLA51o6ikpm2d58fTC0dSWQqoHlfpqtCNe68YNAc40lrUl%21K5s42VZ%21sK5M0J3M0b&Bsrc=EMINGM&Bpub=SN.Notifications>
""
View invitation
<https://profile.live.com/cid-fee5726b043f694d/?invite=dffafc49b6d74ab42%3acTO%2frcTllE8ULIZ%2bbZ1lNl%2bQL8%2b4MgQLXL11%2bpAu9YyrI5ycqv8QTKCCTiP41lrs8HJpfihiBMVkXUedyDIbCfick2kVilRs456JOIJ0%2bbGxlHG2lAcO9mnb%2b0YUyk6C&ids=ChseM4InGnCmhXO%21WXdtt7%21LrheJ4zuyCEkIDX8OqJ%2ah%2auy6JYexgFQ2iB4oVSq4DJbEbZp62be056Q3UQaSEYihlh0%2aB0tA16BGj4sE6%214yLA51o6ikpm2d58fTC0dSWQqoHlfpqtCNe68YNAc40lrUl%21K5s42VZ%21sK5M0J3M0b&Bsrc=EMINGM&Bpub=SN.Notifications>
Notifications preferences
<https://profile.live.com/options/notifications/>
Microsoft privacy statement
<http://g.msn.com.ph/2privacy/ensg>
Microsoft Corporation, One Microsoft Way, Redmond, WA 98052

Announcement

Agata Ciabattoni — 2011-09-27T12:34:22

2-YEAR POSTDOCTORAL POSITION ON STRUCTURAL PROOF THEORY

* The Vienna University of Technology is looking to recruit one
   Postdoctoral Research Assistant to work on the FWF-funded
   project "Nonclassical Proofs: theory, applications and tools", under the
   direction of Agata Ciabattoni.
* The work will take place within the Institute of Computer Languages
   (Theory and Logic group) of the Vienna University of Technology.
* The post is for an appointment of up to 24 months
   and is available from January 2012.
* Applicants should have (or shortly expect to receive) a PhD in
   Mathematics, Computer Science or a closely related field, a strong
   background in structural proof theory, nonclassical logics, and
   knowledge of universal algebra or complexity theory.
   Ability to work independently but also with academic colleagues
   and PhD students, flexibility and teamwork, are all important
   qualifications for this position.
* Further particulars, including details of how to apply, are available
   from: http://www.logic.at/staff/agata/positions.html.
* Potential applicants are also welcome to send informal inquiries to
   Agata Ciabattoni (agata-DX+603jRYB8< at >public.gmane.org)
* The closing date for applications is Thursday, December 1st 2011.

Bruno Woltzenlogel Paleo invited you to join him on Google+

Google+ — 2011-07-11T04:13:58

Bruno Woltzenlogel Paleo is using Google+ and invited you to join.

Click here to get started with Google+:  
https://plus.google.com/_/notifications/emlink?emrecipient=102974918492086419375&emid=CMDr48y2-KkCFUWq7AodrKK2Ag&path=%2Fwelcome%3Fgpinv%3DAGXbFGzWAF-ZnkbkVEP6tpIfJ24_YoCVqvJjcuQVq_hyEPTq9IVnDBZxOcHuE-pp0gtffgAeBxRc05FdirpEGWpBB8w1cJ-KSxUhV_qibJ5YbrXsVptjq5I%26hl%3Den

The Google+ project is currently working out all the kinks with a small  
group of testers. If you're not able to access Google+, please check back  
again soon.
------------------------
You received this message because Bruno Woltzenlogel Paleo invited  
frogs.list< at >gmail.com to join Google+. Click here to unsubscribe from these  
emails:  
https://plus.google.com/_/notifications/emlink?emrecipient=102974918492086419375&emid=CMDr48y2-KkCFUWq7AodrKK2Ag&path=%2Fnonplus%2Femailsettings%3Fgpinv%3DAGXbFGzWAF-ZnkbkVEP6tpIfJ24_YoCVqvJjcuQVq_hyEPTq9IVnDBZxOcHuE-pp0gtffgAeBxRc05FdirpEGWpBB8w1cJ-KSxUhV_qibJ5YbrXsVptjq5I%26est%3DADH5u8Vg7IR8k-J4B5Rw0mnLG6fmG_MYTxPGQP4smrJlmxVWL4GJZXMqOJkeYWeWjeSbD6spZdldFrJR5xRKs52HLuMAtD1kqQ31BrL5L1WA69p1cyAIyrZWVRJKos6rhdSi14S-Mq2HZvkUxfR0sEvAo5i8hLwHsg5m8BQLLr6MdqkNU0ZqOoE%26hl%3Den

Marketing

Alessio Guglielmi — 2011-05-06T19:03:26

Hello,

I recently found that several publications for 
the deep inference page escaped me, so I worked a 
couple of days to catch up. Could you please 
check that everything that could be on 
<http://alessio.guglielmi.name/res/cos/> is 
there, and that what is there is correct?

Also, if you have grants that are not listed, I'd like to know.

This is an appeal to conformism, of course, 
primarily to attract further funding,  mostly for 
postdocs. I'm about to apply for a ~£750,000 
project, we have to shine.

BTW, I don't like hosting the deep inference page 
on a domain with my name (because it seems 
misappropriation, in a way). It's like this only 
because of inertia. I also don't like the idea of 
hosting the stuff on University web pages because 
then they have control on the content. (I bought 
that domain when I realised that I wasn't a free 
man.)

The `open problems' web page is badly badly 
outdated, but it takes a lot of time to collect 
and keep the information organised, I'm 
overwhelmed.

I had to compute some money statistics. So, for 
the curious: excluding PhD, and only from 2006, 
deep inference was the main subject in grants for 
overall £4,190,095.25 (at yesterday's exchange 
rate, in euros it's more). I suppose after four 
millions one loses innocence?

-Alessio

Postdoc position in proof theory in Paris

Lutz Strassburger — 2011-04-25T01:49:34

--------------------------------------------------------
Postdoc position in proof theory in Paris
--------------------------------------------------------

There is an opening of a postdoc position on structural and
computational proof theory. The position is financed by
the ANR within the project STRUCTURAL
<http://www.lix.polytechnique.fr/~lutz/orgs/structural.html>

The postdoc will be hosted by the Laboratoire d'Informatique (LIX) at
the Ecole Polytechnique, one of the "Grand Ecoles" in the French
university system, located in the suburbs of Paris.

Applicants must have a Ph.D. or equivalent in computer science or
mathematics, and should have a strong background in proof theory
and related topics. The principal responsibility of the postdoc
will be to carry out research in the area of proof theory within the
project STRUCTURAL. There are no teaching duties.

For further information, see
<http://www.lix.polytechnique.fr/~lutz/orgs/structural-postdoc.html>

or contact
   Lutz Strassburger <lutz-TgEOGOHWQm0czSlqHMVBIP3zm4ADWneb< at >public.gmane.org>
or
   Kaustuv Chaudhuri <kaustuv.chaudhuri-MZpvjPyXg2s< at >public.gmane.org>

Applications should be sent via email to Lutz Strassburger
<lutz-TgEOGOHWQm0czSlqHMVBIP3zm4ADWneb< at >public.gmane.org> and Kaustuv Chaudhuri
<kaustuv.chaudhuri-MZpvjPyXg2s< at >public.gmane.org>, and should include a CV, a research
statement (1-2 pages), and two recommendation letters. The application
deadline is

*** May 20, 2011 ***

Sophia Strassburger

Alessio Guglielmi — 2011-04-16T13:55:24

Hello,

Sophia Strassburger was born this morning, and everybody is well. She 
will make Lutz a civilised person!

-Alessio

Deeper Cuts in Deep Inference

Bruno Woltzenlogel Paleo — 2011-03-15T18:17:33

Hi!

I noticed that in deep inference (I am having the system SKS in mind), the cut is not as "deep" as it could be. What I mean is the following:

consider the "ai-up" (a.k.a. cut) rule of SKS:

S{~a and a}
----------------
S{ false }

This rule is certainly deep in the sense that it can be applied inside any context S. But it is also shallow in the sense that the cut-formulas do not appear inside any context. I can imagine a "deeper" cut-rule as follows:

S{~a and S'{a}}
--------------------  (1)
S{ S'{false} }

and we could go further and have something like this (which is like a deeper application of modus ponens):

S{(~a or b) and S'{a}}
------------------------------  (2)
S{ S'{b} }

and we can try to go even further and find out what happens when both cut-formulas are within arbitrary contexts:

S{S''{~a} and S'{a}}
--------------------------------------------------------------------------  (3)
S{ ?? }    (any of S{S'{S''{false}}} or S{S''{S'{false}}} ???)


I think that deep modus ponens as formalized by the inference rule (2) above is a quite natural reasoning pattern. I use it all the time, and I think we can also say that theorem provers implicitly use it whenever they are doing deep replacements during, for example, skolemization.

I guess both (1) and (2) could be simulated in SKS by several applications of the switch rule followed by an application of "ai-up", but this would be quite bureaucratic, in my opinion.

Anyway, these are some things that came to my mind while developing a proof format for an SMT-solver (that does skolemization as a pre-processing step), and I haven't thought much about this yet. So, if you have any comments (e.g. whether it has already been investigated somewhere, whether I am out of my mind and it doesn't make sense to investigate it for some reason,...), please let me know...

Best regards,

Bruno

deep inference combinators implementation

Kai Brünnler — 2011-02-16T21:14:54

Hi Frogs,

as an exercise, I've started implementing a interpreter for a little
programming language based on deep inference (in the Curry-Howard sense).
The implementation is in Scala and is shared here on
GitHub<https://github.com/kaibr/dicomb>.
Take a look if you're interested. It can already do amazing things: you
could execute a program that takes an ordered pair and returns its first
component!

Comments and contributions are welcome, of course! I've just barely started,
so it should be easy to get into. I'm currently in the process of
implementing a parser (yes, right now programs are given as abstract syntax
trees), and then I'd like to add lots of example programs to test the
interpreter and the type inference and to experiment with the language.

Oh yes, the paper it is based on is "An Algorithmic Interpretation of a Deep
Inference System" by Richard and myself, available from
here<http://www.iam.unibe.ch/%7Ekai/Papers/2008aidis.pdf>,
if you'd like some background.

Best wishes and maybe happy hacking!

-Kai

Facebook Pages on Logical Subjects

Jon Awbrey — 2011-01-20T16:08:38

Here's an assortment of Facebook pages I created that may
be of interest to Frog people who like that sort of thing:

http://www.facebook.com/pages/Differential-Logic/119559524768107

http://www.facebook.com/pages/Inquiry-Driven-Systems/119515558104734

http://www.facebook.com/pages/Logical-Graphs/110462975683687

http://www.facebook.com/pages/Minimal-Negation-Operators/168166306533929

http://www.facebook.com/pages/Peirce-Matters/159237477450823

http://www.facebook.com/pages/Relation-Theory/163244363703101

http://www.facebook.com/pages/Riffs-Rotes/167712413262717

http://www.facebook.com/pages/Semeiotics/110200632380093

http://www.facebook.com/pages/Theme-One/134629236593886

Jon Awbrey

a.k.a. "Jonny Cache" http://www.facebook.com/people/Jonny-Cache/1039153428

HDR

Lutz Strassburger — 2011-01-07T10:43:33

Hi Frogs,

my habilitation thesis
"Towards a Theory of Proofs of Classical Logic"

is available here:
<http://www.lix.polytechnique.fr/~lutz/papers/HDR.pdf>

The public defense takes place today at 14:00 at Ecole Polytechnique 
(Amphi Bequerel).

Best wishes,
Lutz

REDO meeting in Bath, Sep 14-16

Lutz Strassburger — 2010-08-20T13:10:43

Hi Frogs,

there will be a small meeting on proof theory and related topics in Bath 
from September 14 to September 16.

<http://www.lix.polytechnique.fr/~lutz/orgs/redo-meeting-sep10.html>

Everybody is invited to join.

Since I'll be away from email for the next two weeks, please send an email 
to Alessio Guglielmi (with cc to me) if you are interested in attending 
the meeting or giving a talk.

(Since you are on this mailing list, you have Alessio's email address.)

Best regards,
Lutz

Animated Proofs

Jon Awbrey — 2010-03-14T19:04:45

Hi All --

I finally got around to doing something I've
been thinking about doing since the late 60's,
animating proofs in Peirce's logical graphs.

Here's a rough cut where all I did was flip through
a sequence of images that I had already made up
in storyboard form:

http://mywikibiz.com/Directory:Jon_Awbrey/Papers/Propositional_Equation_Reasoning_Systems#Majority_function_example

Jon Awbrey

Meeting in Vienna

Alessio Guglielmi — 2009-08-05T11:13:35

Hello,

Agata, Lutz and I were thinking of meeting in 
Vienna for a 2/3-day workshop in the period 
24.10-5.11. We are interested in discussing the 
state of the art and perspectives for the proof 
systems of modal and substructural logics.

More in general, the themes should be at least in 
part those of the project Démosthène (Identity 
and Geometric Essence of Proofs) and REDO 
<http://www.lix.polytechnique.fr/~lutz/orgs/redo.html>, 
plus modal logics and whatever interests our 
Austrian hosts.

I liked a lot the format of the recent meeting at 
LIX 
<http://www.lix.polytechnique.fr/~lutz/orgs/redo-meeting-may09.html>, 
so my proposal is to do the same, perhaps on a 
smaller scale.

I would ask the interested people to raise their 
hand and suggest dates (between 24.10 and 5.11), 
so that we can be more specific.

Ciao,

-Alessio

decomposition and splitting for NEL

Lutz Strassburger — 2009-03-30T09:03:10

Hi Frogs,

In preparation for the exciting developments in quantum causal evolution, 
we revised the old paper "A System of Interaction and Structure IV: The 
Exponentials" on the normalisation theory of NEL.

Encouraged from referees, we split the paper into two parts, one about 
decomposition and the other about splitting. We think that this makes the 
whole matter clearer and more accessible. Please do not cite the old 
paper, the new ones are better.

Comments of any kind are very welcome.

Best regards,
Alessio and Lutz

----------------------------------------

Title: A System of Interaction and Structure IV: The Exponentials and 
Decomposition

L. Strassburger and A. Guglielmi

Abstract:
System NEL is the mixed commutative/non-commutative linear logic BV
augmented with linear logic's exponentials, or, equivalently, it is
MELL augmented with the non-commutative self-dual connective
seq. System NEL is Turing-complete, it is able to directly express
process algebra sequential composition and it faithfully models causal
quantum evolution. In this paper, we show a basic compositionality
property of NEL, which we call decomposition. This result leads
to a cut-elimination theorem, which is proved in the next paper of
this series. To control the induction measure for the theorem, we rely
on a novel technique that extracts from NEL proofs the structure of
exponentials, into what we call !-?-Flow-Graphs.

URL: 
<http://www.lix.polytechnique.fr/Labo/Lutz.Strassburger/papers/NEL-decomposition.pdf>

----------------------------------------

Title: A System of Interaction and Structure V: The Exponentials and 
Splitting

A. Guglielmi and L. Strassburger

Abstract:
System NEL is the mixed commutative/non-commutative linear
logic BV augmented with linear logic's exponentials, or,
equivalently, it is MELL augmented with the non-commutative
self-dual connective seq. System NEL is Turing-complete,
it is able to directly express process algebra sequential composition
and it faithfully models causal quantum evolution. In this paper, we
show cut elimination for NEL, based on a property that we call
splitting. NEL is presented in the calculus of structures,
which is a deep-inference formalism, because no Gentzen formalism can
express it analytically. The splitting theorem shows how and to what
extent we can recover a sequent-like structure in NEL proofs.
Together with the decomposition theorem, proved in the previous paper
of the series, this immediately leads to a cut-elimination theorem for
NEL.

URL: 
<http://www.lix.polytechnique.fr/Labo/Lutz.Strassburger/papers/NEL-splitting.pdf>

----------------------------------------

Quasipolynomial normalisation in deep inference

Alessio Guglielmi — 2009-03-25T12:07:49

Hello,

We would like to announce the paper mentioned 
below, which continues a line of work  on 
normalisation in deep inference, where we get 
quasipolinomial normalisation procedures for 
propositional logic. This is essentially due to 
our dealing with a more general notion of 
analyticity than in the sequent calculus, and to 
the novel symmetry of proofs, typical of deep 
inference.

You can find information about deep inference at 
<http://alessio.guglielmi.name/res/cos/>.

Comments are very welcome, of course. Please note 
that the web site where the paper resides will 
not be available during this coming week-end.

Best regards,

-Alessio


Quasipolynomial Normalisation in Deep Inference 
via Atomic Flows and Threshold Formulae
<http://cs.bath.ac.uk/ag/p/QuasiPolNormDI.pdf>
--------------------------------------------------
P Bruscoli, A Guglielmi, T Gundersen and M Parigot

Jerábek showed that analytic propositional-logic 
deep-inference proofs can be constructed in 
quasipolynomial time from nonanalytic proofs. In 
this work, we improve on that as follows: 1) we 
significantly simplify the technique; 2) our 
normalisation procedure is direct, i.e., it is 
internal to deep inference. The paper is 
self-contained, and provides a starting point and 
a good deal of information for tackling the 
problem of whether a polynomial-time 
normalisation procedure exists.