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; ve

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/>
Microsof

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/notifica

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/>
Microsof

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/notifica

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/>
Microsof

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/notifica

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

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%3DADH5u

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 h

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-TgEOGOHWQ

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

Re: Deeper Cuts in Deep Inference

Alessio Guglielmi — 2011-03-17T11:22:31

Hello,

At 21:46 -0300 16/3/11, Bruno Woltzenlogel Paleo wrote:

To clarify: the problem is whether an atomic flow 
and a formula taken as its conclusion, together 
with the association between edges in the flow 
and atom occurrences in the formula, could be 
tested in polynomial time such that the test 
decides if the formula is a tautology.

In other words, the object would be a 
Lamarche-Strassburger proof net with enriched 
identity links, and the problem is to find a 
polynomial-time correctness criterion for it.


1) The flows extracted from proofs have the same 
asymptotic size modulo polynomials (this is a 
fact, the easy paper has been in progress for 
four years but will finally see the light very 
soon).

2) In similar situations in linear proof nets 
polynomial correctness criteria exist.

3) No counterexample emerged yet (but I don't 
know how much effort has been put into this, I 
didn't work on it much myself).


I can't think of any, but I don't understand 
atomic flows very well, so perhaps

Re: Deeper Cuts in Deep Inference

kahramanogullari — 2011-03-17T02:17:46

Hi Bruno,

DPLL
but
moving

It is always possible to add sound and invertible rules to your system to
make it more efficient. However, the main issue here is to achieve
'efficiency' in proof search while preserving as many properties as
possible from those such as modularity, locality, atomicity, symmetry and,
of course, cut-elimination. Splitting technique provides some insight into
this, but in the general setting, this is difficult.

Best regards,
Ozan

Re: Deeper Cuts in Deep Inference

Bruno Woltzenlogel Paleo — 2011-03-17T00:46:16

Hi Alessio,


Ok. Tom was also quite sure that they are.


That's good to know. I hoped so.


Agreed. In principle, to normalize a proof containing the rules I mentioned, we could first replace it by switches and ai^, and then normalize as usual, but of course this wouldn't be as nice as being able to normalize "directly".


What are the arguments in favor of conjecturing that it is a proof system? And what are the arguments against?

Anyway, being a proof system would only mean that its proofs could be checked in polynomial time. Proof search could still be very hard (i.e. if the proof system is not automatizable...)...


In fact, I think that some of the most efficient decision procedures nowadays already use a lot of deep inference. People like to think of DPLL and CDCL as particular strategies for shallow resolution proof search, but things like unit propagation and "decisions" might be more easily understood as a combination of macro-switches and (co)contractions, moving some literals outside the clause

Re:Deeper Cuts in Deep Inference

Alessio Guglielmi — 2011-03-15T20:29:45

Hi Bruno,

If I'm not mistaken, the three rules that you propose are, as you 
say, all derivable via switches and cuts (in the sense of SKS cuts 
ai^). They could be further generalised to generic formulae (instead 
of atoms), and still be derivable via switches and cuts.

Conversely, ai^ is an instance of your rules, of course.

As you say, the difference is in the bureaucracy of the proofs: your 
rules are friendlier from the point of view of proof search. However, 
the vanilla ai^ rule seems more manageable and more fundamental for 
investigating normalisation.

It's perhaps interesting to note that all the bureaucracy disappears 
when one turns to atomic flows [1]: all these rules generate the same 
atomic flows. However, we are still far from being able to use atomic 
flows for proof search (it's an open problem whether atomic flows are 
a proof system).

Ozan Kahramanogullari has done extensive work on the design of 
proof-search friendly proof systems, I think all his papers are 
accessible from the d

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 formalize

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 hack

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

Re: HDR

Laurent Méhats — 2011-01-10T18:09:49

Le 07/01/2011 11:43, Lutz Strassburger a écrit :

Congratulations ! And incidentally, happy new year :)

See you,
Laurent

RE: HDR

Richard Blute — 2011-01-10T08:28:22

I'm sure frogpeople everywhere will be happy to learn that Lutz's habilitation
was a great success. His talk was an excellent advertisement for deep inference 
and categorical logic.

cheers
Rick



________________________________________
From: l. s. [lutz.at.lix-Re5JQEeQqe8AvxtiuMwx3w< at >public.gmane.org] on behalf of Lutz Strassburger [lutz< at >lix.polytechnique.fr]
Sent: Friday, January 07, 2011 5:43 AM
To: Frogs
Subject: [Frogs] HDR

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