View: session overviewtalk overviewside by side with other conferences
09:10  Opening Remarks SPEAKER: unknown ABSTRACT. Welcome to the Third International Workshop on Structures and Deduction. 
09:15  Simply Typed LambdaCalculus Modulo Type Isomorphisms SPEAKER: Gilles Dowek ABSTRACT. In this talk, I will present an extension of simplytyped lambdacalculus where isomorphic types are identified. This requires to introduce new reduction rules, some of which are non deterministic. The normalization of this system is a nontrivial adaptation of the reducibility method.

10:45  Completions and the Schuette method SPEAKER: Rosalie Iemhoff ABSTRACT. The cutelimination theorem of Gerhard Gentzen is one of the most beautiful and useful theorems in structural proof theory. For certain logics there is an algebraic view on cutelimination in which this property is proved via completions of certain semialgebraic structures corresponding to cutfree sequent calculi. There is, however, for intuitionistic propositional logic another way to obtain Heyting algebras refuting an underivable sequent, the socalled Schuette method. We describe this method and compare it to the method of producing algebras via completions. 
11:45  A Correctness Criterion Free from Switchings SPEAKER: unknown ABSTRACT. We present a new correctness criterion for Multiplicative Linear Logic (MLL) proof nets. Our criterion generalizes a criterion recently introduced by Mogbil and Jacobé de Naurois in order to characterize the space complexity of the correctness problem for M(E)LL: while the MogbilNaurois criterion relies on a single switching, our criterion completely abstracts from the notion of switchings. This is done in two steps. First we define dependency graphs on proof nets rather than correction graphs, as in MogbilNaurois, making them switchingindependent. Then, we partition our criterion in two parts: one part deals exclusively with tensor, axiom and cut inferences while the other one deals with the structure of par inferences by requiring dependency graphs to be acyclic flowgraphs (or SDAG). We finally compare both notions of dependency graphs. 
12:15  Firstorder Proofs Without Syntax: Summary of Work in Progress SPEAKER: Dominic Hughes ABSTRACT. "...mathematicians care no more for logic than logicians for mathematics."  Augustus de Morgan, 1868 Formal proofs are traditionally syntactic, build inductively from symbolic inference rules. This paper reformulates classical firstorder logic with proofs which are combinatorial rather than syntactic. A *combinatorial proof* of a formula F is a graph on a variant formula F′ which satisfies geometric properties. For example, an edge between the two Ps in ∀xPx ⇒ ∃x∀yPy constitutes a combinatorial proof of ∃x(Px ⇒ ∀yPy). Combinatorial proofs provide a canonical abstraction of Gentzen’s sequent calculus LK: (a) the correctness of a combinatorial proof can be verified in polynomial time (conjectured linear), and (b) there is a function from LK proofs to combinatorial proofs which identifies many LK proofs. This paper summarizes ongoing work on a sequel to Proofs Without Syntax [Annals of Mathematics, 2006], which introduced propositional combinatorial proofs. 
14:30  Proof theory for ordered algebra: amalgamation and densification SPEAKER: Kazushige Terui ABSTRACT. Proof theory plays only a limited role in the context of superintuitionistic/substructural logics. We certainly have cut elimination, disjunction property, Herbrand's theorem, interpolation and density elimination. But is there anything else? Our purpose is to find further applications of proof theory by making it directly act on algebras (Heyting/FL algebras) rather than on syntactic formulas and proof systems. 
15:30  Weak topologies for Linear Logic SPEAKER: Marie Kerjean ABSTRACT. We construct a categorical model of Linear Logic, whose objects are all the locally convex and separated topological vector spaces endowed with their weak topology. Linear proofs are interpreted as continuous linear functions, and nonlinear proofs as sequences of monomials. The duality in this interpretation of Linear Logic does not come from an orthogonality relation, thus we do not complete our constructions by a doubleorthogonality operation. This yields into an interpretation of polarities with respect to weak topologies. 
16:30  Substructural Cut Elimination SPEAKER: Taus BrockNannestad ABSTRACT. In the paper ``Structural Cut Elimination'', Pfenning gives a proof of the admissibility of cut for intuitionistic and classical logic. The proof is remarkable in that it does not rely on difficult termination metrics, but rather a nested lexicographical induction on the structure of formulas and derivations. A crucial requirement for this proof to go through is that contraction is not an inference rule of the system. Because of this, it is necessary to change the inference rules so that contraction becomes an admissible rule rather than an inference rule. This change also requires that weakening is admissible, hence it is not directly applicable to logics in which only contraction is admissible (e.g. relevance logic). We present a sequent calculus which admits a unified structural cut elimination proof that encompasses Intuitionistic MALL and its affine, strict and intuitionistic extensions. A nice feature of the calculus is that, for instance, moving from linear to strict logic is as simple as allowing the presence of a rule corresponding to contraction. 
17:00  Multiplicative Decomposition of Behaviours in Ludics SPEAKER: unknown ABSTRACT. Ludics is a theory that may be considered, at first glance, as a BrouwerHeyting Kolmogorov interpretation of Logic as a formula is denoted by the set of its proofs. More primitively, Ludics is a theory of interaction that models (a variant of) secondorder multiplicativeadditive Linear Logic. A formula is denoted by a set of objects called a behaviour, a proof by an object that satisfies some criteria. Our aim is to analyze the structure of behaviours in order to better understand and refine the usual notion of formula or type. More precisely, we study properties that guarantee a behaviour to be multiplicatively decomposable. 