Proof Theory Group at TU Dresden / Events
This page is no longer updated.
Proof Theory Group at TU Dresden
Events



In the following list of events, I indicate in square brackets the sources of financing for each event (see also the bottom of the page). Only financing from our sources is indicated. I don't list talks internal to our group and at the local graduate college. I list talks of former group members if they relate to work they carried on while in Dresden.

2005
1.9
Alessio and Paola move to the University of Bath.
9-12.8
Kai (Bern) visits us.
19-22.7
Ozan participates in the WoLLIC 2005 conference (Florianópolis - Brazil) and talks about System BV Is NP-Complete.
16-17.7
Charles and Paola co-organise the workshop Structures and Deduction at next ICALP 2005 in Lisbon; at the workshop, Alessio talks about The Problem of Bureaucracy and Identity of Proofs from the Perspective of Deep Inference, Charles and Robert about Purity Through Unravelling and Ozan about Implementing Deep Inference in TOM.
17.6
Alessio visits Thomas Streicher (TU Darmstadt) and talks about The How and Why of Deep Inference.
15-16.6
Alessio visits Lutz Straßburger at the Programming Systems Lab (Saarbrücken) and talks about Classical Logic in Deep Inference and Some Ideas on Proof Search.
2-7.5
Michel Parigot (PPS group, Paris) visits us.
[CL]
20-21.4
Alessio visits Michel Parigot (PPS group) in Paris.
31.3-3.4
Ozan participates in the UNILOG 2005 conference (Montreux) and talks about Labeled Event Structure Semantics of Linear Logic Planning.
23.3
Robert successfully defends his MSc thesis Geometric Theories and Modal Logic in the Calculus of Structures and he gets the grade 1.0 (the highest possible).
21-24.2
We organise the ICCL Workshop Proof Theory 2005; the following guests visit us:
Yves Guiraud (Marseille)
Lutz Straßburger (Saarbrücken)
Kai Brünnler (Bern)
Richard McKinley (Bath)
Alwen Tiu (LORIA, Nancy)
[CL]
14-16.2
Ozan participates in the AIA 2005 conference (Innsbruck) and talks about Towards Planning as Concurrency.
7.2
Alessio visits the computer science department at University of Bath and gives a talk about Deep Inference.

2004
9-15.12
Alessio visits the PPS group in Paris, participates in the Paris-Vienna Workshop 2004 on Proofs and talks about Reasons and Methods of Deep Inference.
29.11-3.12
Charles and Robert visit INRIA's Calligramme group in Nancy; Charles talks about Designing Proof Theories: Handling Modalities and Labels and Robert talks about 3/4s Scott-Lemmon Theories.
[Proc]
22.11-17.12
Ozan visits INRIA's Calligramme and Protheo groups in Nancy and gives a talk about Implementing Deep Inference.
[Proc]
27-29.10
Ozan participates in the ISCIS 2004 conference (KemerAntalya) and talks about System BV without the Equalities for Unit.
27.10
Phiniki successfully defends her MSc thesis The Design of Modal Proof Theories: The Case of S5 and she gets the grade 1.0 (the highest possible); she joins as a graduate student Gerhard Jäger's group in Bern.
27-28.9
We organise the ICCL Workshop Proof Theory 2004; the following guests visit us:
Roy Dyckhoff (St Andrews)
Nissim Francez (Technion Haifa)
Michel Parigot (CNRS, Paris)
Stéphane Lengrand (St Andrews and Paris VII)
Lutz Straßburger (LORIA, Nancy)
Kai Brünnler (Bern)
Ugo Dal Lago (Bologna)
Jeremy Dawson (NICTA, Canberra)
Birgit Elbl (Universität der Bundeswehr München)
José Espírito Santo (Universidade do Minho)
Elaine Pimentel (Belo Horizonte and Torino)
François Lamarche (Loria & INRIA, Nancy)
[CL]
9-11.9
Charles and Phiniki participate in the AiML 2004 conference (Manchester) and talk about A Systematic Proof Theory for Several Modal Logics.
[CL]
16-20.8
Alessio participates in the ESSLLI 2004 school (Nancy) and lectures on The Calculus of Structures.
[Proc]
9-20.8
Ozan participates in the ESSLLI 2004 school (Nancy) and talks about Implementing System BV of the Calculus of Structures in Maude.
14-25.6
We organise the ICCL Summer School 2004 - Proof Theory and Automated Theorem Proving; the following guests visit us and participate as indicated:
Roy Dyckhoff (St Andrews) gives an invited lecture on Sequent Calculi for Some Non-classical Logics.
Claude Kirchner (Loria & INRIA, Nancy) lectures on Deduction Modulo.
John Slaney (NICTA, Canberra and Australian National University) lectures on Automated Reasoning for Substructural Logics.
Michel Parigot (CNRS - Université Paris 7) lectures on Proofs as Programs.
François Lamarche (Loria & INRIA, Nancy) lectures on Logic Considered as a Branch of Geometry.
Andrei Voronkov (Manchester) lectures on Automated Theorem Proving for Classical Logics.
Luke Ong (Oxford) lectures on Game Semantics and Its Applications.
Simona Ronchi della Rocca (Torino) gives an invited lecture on A Logic for Intersection Types.
Wolfgang Bibel (TU Darmstadt and Un. British Columbia) gives an invited lecture on Transition Logic.
In addition:
Franz Baader (TU Dresden) lectures on Term Rewriting Systems.
Alessio lectures on Deep Inference and the Calculus of Structures.
[CoLogNet, DAAD, GK]
3.6
Alessio visits the PPS group in Paris and gives a talk about Deep Inference and Self-dual Non-commutativity.
13.5
Lutz visits the SIGNES group in Bordeaux and gives a talk about The Calculus of Structures.
31.3-3.4
Alessio participates in the Workshop on Constructive Classical Logic (Roma) and talks about The Need for Deep Inference in Proof Theory.
22-23.3
Lutz visits the Laboratoire de Géométrie, Topologie et Algèbre in Montpellier and gives two talks about Linear Logic in the Calculus of Structures and On Proof Nets for Multiplicative Linear Logic with Units.
1-5.3
Lutz participates in the 9th Estonian Winter School in Computer Science (Palmse) and talks about The Calculus of Structures.
1-5.3
Prakash Panangaden (McGill and Oxford University) visits us and talks about Concurrent Common Knowledge : Agreement and Causal Consistency in Distributed Systems.
[CL]
12.2
Lutz visits the PPS group in Paris and gives a talk about The Calculus of Structures.
26-27.1
Lutz participates in the Géométrie du Calcul meeting (Marseille) and talks about The Calculus of Structures.

2003
11-12.12
Kai participates in the Arbeitstagung Bern-München (München) and gives a talk on Interpolation as Symmetric Cut Elimination.
9-13.12
Paola participates in the ICLP 2003 conference (Mumbai) with the invited tutorial A Tutorial on Proof Theoretic Foundations of Logic Programming.
[CL]
24-26.11
Paola visits INRIA's Calligramme group in Nancy and talks about Linear Logic Proofs Via Macro Rules.
[Proc]
19-21.11
We organise a Workshop on Structural Proof Theory; the following guests visit us:
[CL, IQN, Proc]
12.11
Robert Hein joins the group as a MSc student, supervised by Charles.
29-30.10
Kai participates in the annual meeting of the Swiss Society for Logic and Philosophy of Science (Murten) and gives an invited talk on Deep Inference and Symmetry in Deductive Systems.
6-10.10
Alessio, Charles and Phiniki visit INRIA's Calligramme group in Nancy; Alessio talks about A New Proof Theory with Deep Inference and Symmetry, Charles talks about Partial Sharing Diagrams and Phiniki talks about Modal Logics in the Calculus of Structures.
[Proc]
1.10
Kai joins as a post-doc Gerhard Jäger's group in Bern.
22-26.9
Paola participates in the LPAR 2003 conference (Almaty) and talks about On Structuring Proof Search for First Order Linear Logic.
[CL, HWP]
22.9
Kai defends his PhD thesis Deep Inference and Symmetry in Classical Proofs and gets the grade `summa cum laude´ (the highest possible).
22.9
Dale Miller (INRIA and École Polytechnique, Paris) visits us and talks about Reasoning About Proof Search Specifications.
[GK]
18-21.9
Charles and Kai participate in the FOL75 conference (Berlin); Kai talks about A Finitary System for First Order Logic.
[GK]
1.9
Lutz joins as a post-doc INRIA's Calligramme group in Nancy.
18-30.8
Kai participates in the ESSLLI 2003 school and CSL 2003 conference (Vienna) and, in the conference, he talks about Atomic Cut Elimination for Classical Logic.
[GK]
29.7-1.8
Lutz participates in the WoLLIC 2003 conference (Ouro Preto) and talks about System NEL Is Undecidable.
[GK]
24.7
Lutz successfully defends his PhD thesis Linear Logic and Noncommutativity in the Calculus of Structures and he gets the grade `summa cum laude´ (the highest possible).
23-25.7
François Lamarche (Loria & INRIA-Lorraine, Nancy) visits us.
[Proc]
9.7
Kai visits Gerhard Brewka in Leipzig and gives a talk about Deep Inference and Symmetry in Classical Proofs.
23.6-4.7
We organise a Summer School and Workshop on Proof Theory, Computation and Complexity; the following guests visit us and participate as indicated:
Alwen Tiu (Penn State, USA) talks about Induction and Coinduction in Sequent Calculus.
Birgit Elbl (Universität der Bundeswehr München) talks about Goal Composition and Local Variables.
Roy Dyckhoff (St Andrews) lectures on Term-rewriting and Termination in Proof Theory.
Peter Aczel (Manchester) lectures on Dependent Type Theories.
Jan von Plato (Helsinki) lectures on Natural Deduction: Some Recent Developments.
Isabel Oitavem (Universidade de Lisboa) talks about Characterising PSPACE with Pointers.
Sara Negri (University of Helsinki and Academy of Finland) lectures on Proof Analysis.
Reinhard Kahle (Universidade Nova de Lisboa) lectures on Applicative Theories and Explicit Mathematics.
Stephen Simpson (Penn State, USA) lectures on Mass Problems.
Jim Lipton (Wesleyan, USA) lectures on Semantics and Cut-elimination for Church's (Intuitionistic) Theory of Types, With Applications to Higher-order Logic Programming.
Achim Jung (Birmingham) lectures on Denotational Semantics of Lambda Calculi.
In addition:
Lutz talks about System NEL Is Undecidable.
Charles talks about Is Deep Inference Necessary for Good Proof Theoretic Treatments of Modal Logic?
Kai talks about Interpolation as Symmetric Cut Elimination.
Alessio lectures on Proof Theory with Deep Inference.
[CGIL, CoLogNet, DAAD, GK, IQN]
16-18.4
Kai visits Gerhard Jäger in Bern and gives a talk about Deep Inference and Symmetry in Classical Proofs.
17-20.3
Jim Lipton (Wesleyan, USA) visits us and talks about Cut Elimination and Completeness of Higher Order Intuitionistic Logic.
[CL]
6-7.3
Alessio visits Giorgio Levi in Pisa and gives a talk about Deep Inference.
[CL]
14-17.2
Charles participates in the Foundations of the Formal Sciences IV conference (Bonn) and talks about Conceptual Harmony and the Semantics of Programming Languages.
9.2
Ozan Kahramanogullari joins the group as a PhD student, supervised by Steffen and Gerhard Brewka.
5-9.2
Kai visits Stefano Guerrini in Roma and gives a talk about Atomic Cut Elimination for Classical Logic.
[GK]
29.1
Heinrich Wansing (TU Dresden) visits us for a discussion about deep inference, display calculus and modal logic.
15-21.1
Lutz visits François Lamarche in Nancy and gives a talk about The Calculus of Structures.
[Proc]

2002
11-13.12
Lutz and Paola participate in the 17. WLP - Workshop Logische Programmierung (Dresden) with two talks: Linear Logic and Non-commutativity in the Calculus of Structures and A Purely Logical Account of Sequentiality in Proof Search.
4-12.12
Kai visits Giorgio Levi in Pisa and Simone Martini in Bologna and gives talks about Classical Logic in the Calculus of Structures.
[GK]
16-20.11
Charles visits Luke Ong in Oxford and Thomas Forster in Cambridge.
[GK]
11.11
Phiniki Stouppa joins the group as a MSc student, supervised by Charles.
14-18.10
Lutz participates in the LPAR 2002 conference (Tbilisi) with two talks: A Non-commutative Extension of MELL and A Local System for Linear Logic.
[GK]
25.8-15.9
Charles visits Harry Mairson at Brandeis University (Boston).
5-16.8
Kai participates in the ESSLI 2002 school (Trento).
[GK]
29.7-1.8
Paola participates in the ICLP 2002 conference (Copenhagen) and talks about A Purely Logical Account of Sequentiality in Proof Search.
[CL, HWP]
23-30.7
Kai visits Michel Parigot at Paris 7.
15.7
Charles Stewart joins the group as a researcher.
[GK]
8-13.6
Michel Parigot (Paris 7) visits us.
[IQN]
7.6-31.7
Alwen Tiu (Penn State) visits us.
[IQN]
3-14.6
We organise a Workshop on Proof Theory and Computation; the following guests visit us and participate as indicated:
Yves Lafont (Marseille) lectures on Algebraic Theory of Circuits.
François Lamarche (Loria & INRIA-Lorraine, Nancy) lectures on Operads and the Geometry of Computation and talks about The Need for Reversible Syntax.
Birgit Elbl (Universität der Bundeswehr München) talks about A Framework for Symbolic Predicational Languages.
Dale Miller (Penn State) lectures on Specifying and Reasoning about Programs in Proof Search.
Catuscia Palamidessi (Penn State) lectures on Formal Methods for Security Protocols.
S. Arun-Kumar (IIT Delhi) talks about Reflecting BDDs in Coq.
Charles Stewart (TU Berlin) lectures on Harmonic Type Theory and talks about Compiling with Graph Transformations.
In addition:
Pascal Hitzler (TU Dresden) talks about Fixed Point Semantics for Logic Programming and Non-monotonic Reasoning: A Uniform Approach.
Alessio lectures on The Calculus of Structures.
[CL, GK, IQN]
8-9.4
Alessio, Kai and Lutz participate in the Proof, Computation, Complexity workshop (Tübingen) with two talks: The Calculus of Structures and A Local System for Linear Logic.
[CL, GK]
1-8.3
Kai participates in the Interdisziplinäres Kolleg 2002 school (Günne).
[GK]
28.1-8.2
Lutz participates in the Logic & Interaction Weeks meeting (Marseille).
[GK]

2001
13.11
Philippe de Groote talks about Abstract Categorial Grammars.
[CL]
11-30.11
Philippe de Groote (INRIA Lorraine, Nancy) visits us and teaches Introduction to Typed Lambda Calculus and Proof Theory.
[CL]
3-7.12
Kai participates in the LPAR 2001 conference (La Habana) and talks about A Local System for Classical Logic.
[GK]
6-9.11
Charles Stewart (TU Berlin) visits us and talks about Logics, Graphs and the Lambda Calculus.
[CL]
25.9
Alwen talks at the Penn State Logic Seminar about A Logical System That Challenges Sequent Calculus.
10-13.9
Lutz participates in the CSL 2001 conference (Paris) and talks about Non-commutativity and MELL in the Calculus of Structures.
[GK]
13.8-24.8
Lutz participates in the 13th European Summer School in Logic, Language and Information (ESSLLI 2001) (Helsinki).
1.8
Alwen successfully defends his MSc thesis Properties of a Logical System in the Calculus of Structures and he gets the grade 1.0 (the highest possible); he then joins Penn State University as a PhD student, supervised by Dale Miller.
24.7-5.8
Kai participates in the Marktoberdorf Summer School 2001 and talks about Atomic Contraction.
[GK]
31.5-3.6
Yves Lafont (Marseille) visits us and talks about The Paradigm of Interaction.
[CL]
30.5-3.6
Birgit Elbl (Universität der Bundeswehr München) visits us and talks about A Class of Substructural Calculi with Context-dependent Rules: Application and Proof-theoretic Properties.
[CL]
28.5
Lutz visits Maurizio Martelli in Genova and gives a talk about MELL in the Calculus of Structures.
[GK]
21.5-26.5
Lutz participates in the 6th International Summer School on Distributed Computing (Isola d'Elba, Italy).
[GK]
18.5
Lutz visits Giorgio Levi in Pisa and gives a talk about MELL in the Calculus of Structures.
[GK]
2.5
Achim Jung talks about Denotational Semantics with Relational Models.
[CL]
23.4-4.5
Achim Jung (Birmingham) visits us and teaches Domain Theory and Applications.
[CL]
16-19.4
Giorgio Levi (Pisa) visits us and talks about A Systematic Approach to Program Analysis and Verification.
[CL]
5-9.2
Kai and Lutz participate in the Spezifikation Diskreter Prozesse und Prozesssysteme Durch Operationelle Modelle und Logiken workshop (Reinhardtsdorf) and give two talks about Classical Logic in the Calculus of Structures and Sequent Calculus for MELL.
[GK]

2000
8.12
We organise a Workshop in Proof Theory; talks:
[CL]
7-9.12
Charles Stewart (Boston and Brandeis Universities) visits us.
[CL]
6-8.12
Didier Galmiche (LORIA, Nancy) visits us.
[CL]
29.11-3.12
Dale Miller (Penn State) visits us and talks about Encoding Transition Systems in Sequent Calculus.
[CL]
12.11-17.12
Roy Dyckhoff (St Andrews) visits us and teaches Structural Proof Theory.
[CL]
1.11
Kai Brünnler joins the group as a PhD student, supervised by Alessio.
[GK]
30.8-7.9
Alwen, Kai Brünnler and Lutz participate in the Linear International Summer School (Linear Logic and Applications) (S. Miguel, Azores).
[CL]
30.8
Alwen Tiu joins the group as a MSc student, supervised by Alessio.
1.7
Lutz Straßburger joins the group as a PhD student, supervised by Alessio.
[GK]
26-27.4
Alessio visits Wolfgang Bibel at TU Darmstadt and talks about A Calculus of Order and Interaction.
27.3-2.4
Pietro Di Gianantonio (Udine) visits us and talks about A Golden Ratio Notation for the Real Numbers.
[CL]
14.3
Charles Stewart (Boston and Brandeis Universities) visits us and talks about Interaction Nets: A Bridge from Theory to Practice.
[CL]

1999
22.6
Jim Lipton talks about Categories and Logic Programming.
[CL]
21.6-7.7
Jim Lipton (Wesleyan, USA) visits us and teaches Modelling and Using Logic Programming Extensions.
[CL]
27-28.5
Alessio and Paola participate in the Logik in der Informatik workshop (TU Dresden) and talk about A Calculus of Order and Interaction and Proof Search and Non-determinism in First Order Linear Logic.

1998
14-15.12
Alessandro Provetti (Milano) visits us and talks about The Stable Models of Unstratified Programs.
[CL]
24.11
Giorgio Levi talks about From Denotational Semantics to Compiled Code.
[CL]
23.11-4.12
Giorgio Levi (Pisa) visits us and teaches Abstraction in Logic Programming.
[CL]

Events are financed by:
[CGIL]
Consolato Generale d'Italia - Lipsia/Italienisches Generalkonsulat in Leipzig
[CL]
International Masters Programme in Computational Logic
[CoLogNet]
CoLogNet
[DAAD]
Deutscher Akademischer Austausch Dienst
[GK]
Graduiertenkolleg 334 Spezifikation Diskreter Prozesse und Prozesssysteme Durch Operationelle Modelle und Logiken
[HWP]
Sächsische Ministerium für Wissenschaft und Kunst Programme HWP
[IQN]
International Quality Network Rational Mobile Agents and Systems of Agents
Exclusive grant:
[Proc]
DAAD grant Procope Structures and Deductions, for scientific exchanges with INRIA's group Calligramme, in 2003 and 2004 (total amount for our group 7400 EUR, Calligramme has separate funding)

10.8.2005
Alessio Guglielmi
email