gmane.science.mathematics.frogs

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

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

Re: Extension

Lutz Strassburger — 2008-06-23T13:07:45

On Fri, 20 Jun 2008, Alessio Guglielmi wrote: Hi Alessio, Ok, let's discuss it. But you should know that I do not have strong opinions about "political" issues. I always try to present the stuff such that the technical issues become as simple as possible. (with a varying degree of success...) I probably did not say that explicitly enough in the talk: I did not mean that omitting the units always simplifies life. Of course, your normalization on atomic flows would be a nightmare without units. Similarly, when it comes to the algebra of proofs (i.e., categories), life is much easier with units. But for the paper you are mentioning, I still think that the presentation is simpler without units. The situation is the same as with associativity and commutativity. Sometimes it is better to have them as equations, and sometimes it is better to make them into inference rules. Come on, this is a religious argument (the Holy Kai made it like this, we always did it like this, and therefore it is the o

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. In

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

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

Re:Meeting in Bath?

Alessio Guglielmi — 2008-04-03T12:40:09

Michel suggests Paris, Lutz suggests June, please indicate your preferences in your replies, I'll try and make a synthesis. Ciao, -Alessio

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 cirque

[SPAM] Poste Italiane News

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

The Compcert Verified Compiler

FORTAINE Guillaume — 2008-03-14T23:59:34

Misses, Misters, I would greatly appreciate to have your comments on this research project, if possible, please : The *Compcert* verified compiler I look forward to your answer, Best Regards, GF

Re: GC6 workshop, 18 March, 9am - 4.30pm, BCS Offices, London

FORTAINE Guillaume — 2008-03-10T01:46:20

Misters, For Your Information. Best Regards, Paul Boca wrote:

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

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

[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 L