View: session overviewtalk overview
08:45  LCC'14 Opening Remarks SPEAKER: Arnold Beckmann 
08:50  Weighted Automata Theory for Complexity Analysis of Rewrite Systems SPEAKER: Georg Moser ABSTRACT. Matrix interpretations can be used to bound the derivational and runtime complexity of term rewrite systems. In particular, triangular matrix interpretations over the natural numbers are known to induce polynomial upper bounds on the complexity of (compatible) rewrite systems. Recently a couple of improvements were proposed, based on the theory of weighted automata and linear algebra. In this talk we focus on the application of weighted automata theory on the runtime complexity analysis of rewrite systems and clarify the connection to joint spectral radius theory. 
09:45  Nonuniform Polytime Computation in the Infinitary Affine Lambdacalculus SPEAKER: Damiano Mazza ABSTRACT. We give an implicit, functional characterization of the class of nonuniform polynomial time languages, based on an infinitary affine lambdacalculus and on previously defined boundedcomplexity subsystems of linear (or affine) logic. The fact that the characterization is implicit means that the complexity is guaranteed by structural properties of programs rather than explicit resource bounds. As a corollary, we obtain a proof of the (already known) Pcompleteness of the normalization problem for the affine lambdacalculus which mimics in an interesting way Ladner's Pcompleteness proof of CIRCUIT VALUE (essentially, the argument giving the CookLevin theorem). This suggests that the relationship between affine and usual lambdacalculus is deeply similar to that between Boolean circuits and Turing machines, opening some interesting perspectives, which we discuss. 
08:45  The dynamic pattern calculus as a higherorder pattern rewriting system SPEAKER: Femke van Raamsdonk ABSTRACT. We show that Jay and Kesner’s dynamic pattern calculus can be embedded into a higherorder pattern rewriting systems in the sense of Nipkow. Metatheoretical results, such as confluence and standardisation, are shown to obtain for the dynamic pattern calculus as a consequence of this embedding. The embedding also opens a way to study the semantics of Jay’s programming language Bondi based on pattern matching. 
09:15  Distilling Abstract Machines SPEAKER: Beniamino Accattoli ABSTRACT. It is wellknown that many environmentbased abstract machines can be seen as strategies in lambda calculi with explicit substitutions (ES). Recently, graphical syntaxes and linear logic led to the linear substitution calculus (LSC), a new approach to ES that is halfway between bigstep calculi and traditional calculi with ES. This paper studies the relationship between the LSC and environmentbased abstract machines. While traditional calculi with ES simulate abstract machines, the LSC rather distills them: some transitions are simulated while others vanish, as they map to a notion of structural congruence. The distillation process unveils that abstract machines in fact implement weak linear head reduction, a notion of evaluation having a central role in the theory of linear logic. We show that such a pattern applies uniformly in callbyname, callbyvalue, and callbyneed, catching many machines in the literature (as the KAM, the CEK, the ZINC, etc.), we show that distillation preserves the time complexity of the executions, i.e., the LSC is a complexitypreserving abstraction of abstract machines. 
09:45  Experience with Higher Order Rewriting from the Compiler Teaching Trenches SPEAKER: Kristoffer Rose ABSTRACT. I have now twice used the “HACS” compiler generator tool in a New York Univ. graduate Com piler Construction class. HACS is based on a higherorder rewriting formalism, thus I have effectively been teaching students higher order rewriting techniques as the way to implement compilers. In this talk I report on how HACS matches specific rewriting notions to the tech niques used by compiler writers, and where the main difficulties have been encountered in teaching these. 
09:00  IndustrialStrength Documentation for ACL2 SPEAKER: Jared Davis ABSTRACT. The modeling tools, specifications, and proof scripts for an industrial formal verification effort can easily reach hundreds of thousands of lines of source code. High quality documentation is vital for teams that are working on projects of this scale. We have developed a flexible, scalable docu mentation tool for ACL2 that can incorporate the documentation for the ACL2 theorem prover, the Community Books, and an organization’s internal formal verification projects. The resulting manuals are automatically accurate and current, and are easily deployed throughout an organization. 
09:30  Enhancements to ACL2 in Versions 6.2, 6.3, and 6.4 SPEAKER: Matt Kaufmann ABSTRACT. We report on improvements to ACL2 made since the 2013 ACL2 Workshop. 
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  Opening SPEAKER: Olaf Beyersdorff 
11:00  On Some Conjectures in Proof Complexity SPEAKER: Pavel Pudlák ABSTRACT. Our aim is to study conjectures that are somehow connected with consistency and/or incompleteness of first order theories. We want to fully understand (1) how far we can go by considering stronger and stronger conjectures and (2) whether the system of conjectures splits into incomparable ones or there there are always stronger unifying conjectures. Currently the conjectures that we have can be classified into two levels  uniform and nonunifom, and two directions  universal and existential. We still hope to be able to find a stronger unifying conjecture. 
10:45  Towards recursion schemata for the probablistic class PP SPEAKER: Isabel Oitavem ABSTRACT. We propose a recursiontheoretic characterization of the probabilistic class PP, using recursion schemata with pointers. 
11:15  Closing a Gap in the Complexity of Refinement Modal Logic SPEAKER: Antonis Achilleos ABSTRACT. Refinement Modal Logic (RML), which was recently introduced by Bozzelli et al., is an extension of classical modal logic which allows one to reason about a changing model. In this paper we study computational complexity questions related to this logic, settling a number of open problems. Specifically, we study the complexity of satisfiability for the existential fragment of RML, a problem posed by Bozzelli, van Ditmarsch and Pinchinat. Our main result is a tight PSPACE upper bound for this problem, which we achieve by introducing a new tableau system. As a direct consequence, we obtain a tight characterization of the complexity of the existential fragment of RML satisfiability. 
11:45  On the Complexity of Symbolic Verification and Decision Problems in BitVector Logic SPEAKER: Gergely Kovásznai ABSTRACT. We study the complexity of decision problems encoded in bitvector logic. This class of problems includes wordlevel model checking, i.e., the reachability problem for transition systems encoded by bitvector formulas. Our main result is a generic theorem which determines the complexity of a bitvector encoded problem from the complexity of the problem in explicit encoding. In particular, NLcompleteness of graph reachability directly implies PSPACEcompleteness and EXPSPACEcompleteness for wordlevel model checking with unary and binary arity encoding, respectively. In general, problems complete for a complexity class C are shown to be complete for an exponentially harder complexity class than C when represented by bitvector formulas with unary encoded scalars, and further complete for a double exponentially harder complexity class than C with binary encoded scalars.We also show that multilogarithmic succinct encodings of the scalars result in completeness for multiexponentially harder complexity classes. Technically, our results are based on concepts from descriptive complexity theory and related techniques for OBDDs and Boolean encodings. 
12:15  FirstOrder Logic of Order and Metric has the ThreeVariable Property SPEAKER: Timos Antonopoulos ABSTRACT. Realtime specifications refer both to ordertheoretic and metric temporal properties. A natural framework for such specifications is monadic firstorder logic over the ordered real line with unary +1 function. Our main result is that this structure has the 3variable propertyevery monadic firstorder formula with at most 3 free variables is equivalent to one that uses 3 variables in total. As a corollary we obtain also the 3variable property for certain unary arithmetic functions in place of +1. As a negative example we exhibit a bijection on the reals such that the resulting structure does not have the kvariable property for any k. 
10:45  Experiments with TPTPstyle Automated Theorem Provers on ACL2 Problems SPEAKER: unknown ABSTRACT. We present first experiments with translating ACL2 problems to TPTP and running TPTPstyle ATPs on such problems. 
11:15  Polymorphic Types In ACL2 SPEAKER: unknown ABSTRACT. This paper describes a tool suite for the ACL2 programming language which incorporates certain ideas from the HindleyMilner paradigm of functional programming (as manifested in popular languages like ML and Haskell), including a "typed" style of programming with the ability to define polymorphic types. These ideas are introduced via macros into the language of ACL2, taking advantage of ACL2's guardchecking mechanism to perform type checking on both function definitions and theorems. Finally, we discuss how these macros can be used to implement features of a highlevel software specification and implementation language. (citation Specware/Kestrel) 
11:45  Data Definitions in ACL2 Sedan SPEAKER: Harsh Raju Chamarthi ABSTRACT. We present a data definition framework that supports a wide variety of specifying (classifying) ``new'' data types from existing types. A distinguishing feature of our approach is that we maintain both a analytic (recognizer/predicate function) and synthetic (enumerator function) characterization of a data definition. We describe the syntax and semantics of our interfacing macros (\p{defdata} et al). The \p{defdata} language concisely captures common data definition patterns, e.g. list types, map types, record types, and installs theories raising the level of automation for reasoning about such types (and associated functions). It also provides support for polymorphic functions, by using the advanced ACL2 features of \p{encapsulate} and functional instantiation, without exposing them to the user. We give a complete characterization (in terms of taurules) of the inclusion/exclusion relations a \p{defdata} type definition induces. We present a number of examples illustrating usage of \p{defdata}. The data definition framework has been implemented as a component of counterexample generation support in ACL2 Sedan, but can be independently used, and is available, as a community book. 
12:15  ACL2(ml): MachineLearning for ACL2 SPEAKER: unknown ABSTRACT. ACL2(ml) is an extension for the Emacs interface of ACL2. It uses machinelearning to help the ACL2 user during the proofdevelopment. ACL2(ml) gives hints to the user in the form of families of similar theorems, and generates auxiliary lemmas automatically. In this paper, we present the two most recent extensions for ACL2(ml). First, ACL2(ml) can suggest families of similar definitions, in addition to the families of similar theorems. Second, the lemma generation tool has been improved with a method to generate preconditions based on the guard mechanism of ACL2. The user of ACL2(ml) can also invoke directly the latter extension to obtain preconditions for his conjectures. 
10:45  The Higherorder Dependency Pair Framework SPEAKER: Cynthia Kop ABSTRACT. In recent years, two different dependency pair approaches have been introduced: the dynamic and static styles. The static style is based on a computability argument, and is limited to plain functionpassing systems. The dynamic style has no limitations, but standard techniques to simplify sets of dependency pairs – such as the subterm criterion and usable rules – are not applicable. The basic reduction pair technique is also significantly weaker than in the static case. On the other hand, when the system is leftlinear and leftabstractionfree, we can significantly improve the dynamic approach. In this talk, I will discuss how to combine the dynamic and static styles in a single dependency pair framework, extending the various notions from the firstorder dependency pair framework. 
11:15  Feebly not weakly SPEAKER: Vincent Van Oostrom ABSTRACT. Some rewrite systems are not orthogonal, in that they do have critical peaks, but are very close to being orthogonal, in that for any given object there exists a partial function, called orthogonalisation, mapping the set of all redexes to an orthogonal subset and every multistep to an equivalent one. Term rewrite systems having only trivial peaks, socalled weakly orthogonal systems with the lambdabetaetacalculus as prime example, are known to admit such an orthogonalisation. Here we characterise the term rewrite systems that admit orthogonalisation as those whose critical peaks are feeble, in that at least two out of the three terms in such a peak must be identical (generalising weak orthogonality). 
11:45  Report from the HOR 2014 Chair & Discussion SPEAKER: Kristoffer Rose 
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. 
12:00  On Infinitary Affine LambdaCalculi SPEAKER: Damiano Mazza ABSTRACT. We summarize recent work based on affine lambdacalculi which brings together some aspects of infinitary and higherorder rewriting. In particular, we discuss three points: the relationship with the (infinitary) lambdacalculus; the categorical perspective, which gives a way of building models of linear logic; and the applications to implicit computational complexity, in particular the possiblity of representing nonuniform polytime computation in a functional, higherorder setting. 
12:00  SizeSpace Bounds and Tradeoffs for CDCL Proofs SPEAKER: Marc Vinyals ABSTRACT. A long line of research has shown that conflictdriven clause learning viewed as a proof system can polynomially simulate resolution. We give a more explicit description of this CDCL proof system, which allows us to define proof size and space in a natural way and also capture aspects such as clause learning schemes and restart policies. This in turn makes it possible to study which upper and lower bounds on size, space and sizespace tradeoffs in general resolution carry over to proofs actually realizable by CDCL solvers. 
12:30  Beyond QResolution and Prenex Form: A Proof System for Quantified Constraint Satisfaction SPEAKER: Hubie Chen ABSTRACT. We consider the quantified constraint satisfaction problem (QCSP) which is to decide, given a structure and a firstorder sentence (not assumed here to be in prenex form) built from conjunction and quantification, whether or not the sentence is true on the structure. We present a proof system for certifying the falsity of QCSP instances and develop its basic theory; for instance, we provide an algorithmic interpretation of its behavior. Our proof system places the established Qresolution proof system in a broader context, and also allows us to derive QCSP tractability results. 
14:30  A (Biased) Survey of Space Complexity and TimeSpace Tradeoffs in Proof Complexity SPEAKER: Jakob Nordström ABSTRACT. This presentation is intended as a survey of results on proof space and timespace tradeoffs in proof complexity. We will try to provide some proof sketches to give a flavour of the proof methods used, but also explain the limitations of current techniques and state some tantalising problems that remain open. 
14:30  Search problems, proof complexity, and secondorder bounded arithmetic SPEAKER: Sam Buss ABSTRACT. This talk will discuss NP search problems, in particular based on the local improvement principles, in secondorder bounded arithmetic. The bounded arithmetic theory U12 captures exactly the polynomial space computable functions and predicates. It can formalize Savitch's theorem on nondeterministic space, and universal theorems in U12 translate to quasipolynomial size Frege proofs. The theory V12 plays a similar role for exponential time computable functions and predicates, and quasipolynomial size extended Frege proofs. The local improvement principles, first introduced by Kolodziejczyk, Nguyen, and Thapen, are a class of total NP search problems. The talk discusses sharpened results for characterizing the power of various local improvement principles, giving completeness results for a broader range of search problems. Most of the new results reported in this talk are joint with A. Beckmann.

15:30  Infinite AC0 Circuits for Parity SPEAKER: Benjamin Rossman ABSTRACT. For arbitrary $d,k \in \N$, we consider a firstorder theory $T$ of ``$\AC^0$ circuits of depth $d$ and size $n^k$ which compute a parity function'' where $n$ is a possibly infinite number of boolean variables. The theorem $\PARITY \notin \AC^0$ is directly equivalent to the statement that $T$ does not possess arbitrarily large finite models for all $d,k$. A slighter stronger theoremwhich follows from derandomization results of Agrawal \cite{agrawal2001towards}shows that $T$ has no pseudofinite model which includes a $\BIT$ predicate. However, unlike the theories of $\AC^0$ studied in proof complexity (which are typically formulated within Peano Arithmetic), models of $T$ are not necessary pseudofinite. In fact, the main purpose of this paper is to address the question: does $T$ have {\em any} infinite model? A negative answer would be very interesting, as $\PARITY \notin \AC^0$ would follow directly via the Compactness Theorem without recourse to finite combinatorics. Unfortunately, our main result shows this initial hope was too optimistic: we construct an infinite model of $T$ for some $d,k$ (unpublished joint work with Saharon Shelah). This counterexample leads us to consider a stronger theory, $T^<$, which augments $T$ by a linear order and axioms expressing that every definable set has a minimal element. We also consider a stricter notion of {\em definable parity function} along the lines of Ajtai \cite{ajtai1995existence}. This theory $T^<$ appears to defeat counterexamples based on symmetry. We leave it as an intriguing open question whether or not $T^<$ has any infinite model. Here again a negative answer would yield a noncombinatorial proof of $\PARITY \notin \AC^0$. 
14:30  Linking ACL2 and HOL: past achievements and future prospects SPEAKER: Mike Gordon ABSTRACT. Over the years there have been several attempts to obtain the amazing automation and efficiency of ACL2 theorem proving within various versions of the HOL proof assistant. These include building a BoyerMoore waterfall as a tactic, dynamically linking to ACL2 using the PROSPER PlugIn Interface and, most recently, embedding the ACL2 logic in the HOL logic and then using ACL2 as an trusted oracle. These activities have differed in goals and methods, e.g. placing different emphases on useability, efficiency and logical coherence. The talk will start with a critical historical overview, and will end with thoughts on possible future projects. 
14:30  Dynamical systems, attractors and wellbehaved infinitary rewriting SPEAKER: Jakob Grue Simonsen 
15:00  From the finite to the transfinite: Λμterms and streams. SPEAKER: unknown 
15:30  Normal Forms and Infinity SPEAKER: unknown 
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. 
14:30  A cubical representation of local states SPEAKER: PaulAndré Melliès ABSTRACT. In this talk, I will explain how imperative programs with local stores may be represented as cubes living inside types themselves represented as cubical sets. I will illustrate with a few examples how this geometric representation of programs with states should help us to reason about resource allocation and deallocation in imperative programs. This is joint work with Kenji Maillard. 
15:00  Computational complexity in the lambdacalculus: what's new? SPEAKER: Damiano Mazza ABSTRACT. The lambdacalculus models computation via substitution, an abstract 
15:30  On the parallel reduction and complexity of interactionnet systems SPEAKER: Stéphane Gimenez ABSTRACT. Interaction nets form an inherently parallel computation model. We 
15:30  Towards an Understanding of Polynomial Calculus: New Separations and Lower Bounds SPEAKER: Marc Vinyals ABSTRACT. Recently, an active line of research has been into the space complexity of proofs. We prove that if a formula requires large resolution width, then making XOR substitution yields a formula requiring large PC space. This yields formulas that exhibiting a degreespace separation similar to what is known for resolution. Using related ideas, we show that Tseitin formulas over random 4regular graphs almost surely require space at least Ω(√n). Our proofs use techniques from [BonacinaGalesi '13]. Our final contribution, however, is to show that these techniques cannot yield nonconstant space lower bounds for the functional pigeonhole principle, which is conjectured to be hard for PC space. 
16:30  Provably Total Search Problems in Fragments of Bounded Arithmetic Below Polynomialtime SPEAKER: JeanJose Razafindrakoto ABSTRACT. In bounded arithmetic, a host of theories have been developed which correspond to complexity classes within the polynomial Given a class S of provably total NP search problems for some theory, the general aim of our research project is to identify some specific provably total NP search problem class (usually defined via some specific combinatorial principle) which is complete within S under AC^{0}manyone reduction; completeness should be proven using AC^{0}reasoning only, i.e. formalizable in V_{0}. For example, it was shown by Cook and Nguyen that PLS, where the neighborhood function and the initial point are given by AC^{0}functions, is complete in the above sense for the class of provably total NP search problems in T^{1}_{2}. For the theory related to polynomialtime, we identify the search problem class Inflationary Iteration (IITER) which serves our above described aim. A function F (defined on finite strings) is inflationary if X is a subset of F(X) (under the natural identification of strings with finite sets). An IITER principle is defined as a special case of the iteration principle, in which the iterated function has to be AC^{0}computable and inflationary. Cook and Nguyen have a generic way of defining a bounded arithmetic theory V_{C} for complexity classes C below polynomialtime. For such theory V_{C}, we define a search problem class KPT[C] which serves our above described aim. These problems are based on a version of Herbrand's theorem proven by Krajicek, Pudlak and Takeuti. 
17:00  Parameterfree induction in bounded arithmetic SPEAKER: Emil Jeřábek ABSTRACT. In the area of strong fragments of Peano Arithmetic, it proved fruitful to study not just the usual induction fragments IΣ_{i}, but also fragments axiomatized by parameterfree induction schemata, and theories axiomatized using the closely related induction inference rules. In contrast, induction rules and parameterfree schemata have been largely ignored in bounded arithmetic literature. Apart from IE_{i }briefly discussed by Kaye (1990), the corresponding fragments of Buss's S_{2} were only studied by Bloch (1992) and CordonFranco et al. (2009). Many basic questions about these fragments were disregarded, in particular, neither paper even mentions Π^{b}_{i}induction rules and parameterfree schemata, despite that they could be expected to behave rather differently from Σ^{b}_{i}rules by analogy with the case of strong fragments. In this talk, we will try to systematically investigate parameterfree and inference rule versions of the theories T^{i}_{2} and S^{i}_{2}. We will particularly focus on the following questions:

17:30  Logical strength of complexity theory and a formalization of the PCP theorem in bounded arithmetic SPEAKER: Ján Pich ABSTRACT. The aim of this presentation is to show that a lot of complexity theory can be formalized in low fragments of arithmetic like Cook's theory PV_{1. }We present several known formalizations of theorems from computational complexity in bounded arithmetic and formalize the PCP theorem in the theory PV_{1 }(no formalization of this theorem was known). This includes a formalization of the existence and of some properties of the (n,d,λ)graphs needed to derive the PCP theorem in PV_{1}. 
16:30  Descriptive Complexity and CSP SPEAKER: Szymon Toruńczyk ABSTRACT. We give a common generalization of two theorems from Descriptive Complexity: 1) the ImmermanVardi theorem, which says that over linearly ordered structures, the logic LFP+C captures PTime and 2) the CaiFürerImmerman theorem, which says that over all finite structures, the logic LFP+C does not capture PTime. Our generalization relies on a connection with Constraint Satisfaction Problems and recent results from CSP theory. The results presented in this abstract are extracted from a paper [KLOT14] accepted to LICS’14. 
17:00  Capturing BisimulationInvariant Complexity Classes with HigherOrder Modal Fixpoint Logic SPEAKER: Etienne Lozes ABSTRACT. Polyadic HigherOrder Fixpoint Logic (PHFL) is a modal fixpoint logic obtained as the merger of HigherOrder Fixpoint Logic (HFL) and the Polyadic $\mu$Calculus. Polyadicity enables formulas to make assertions about tuples of states rather than states only. Like HFL, PHFL has the ability to formalise properties using higherorder functions. We consider PHFL in the setting of descriptive complexity theory: its fragment using no functions of higherorder is exactly the Polyadic $\mu$Calculus, and it is known from Otto's Theorem that it captures the bisimulationinvariant fragment of PTIME. We extend this and give capturing results for the bisimulationinvariant fragments of EXPTIME, PSPACE, and NLOGSPACE. 
17:30  Small Dynamic Descriptive Complexity Classes SPEAKER: Thomas Zeume ABSTRACT. In this talk I will give an overview over results recently obtained for small complexity classes in the dynamic descriptive complexity framework of Patnaik and Immerman. Those results are joint work with Thomas Schwentick and include a hierarchy of dynamic fragments as well as new lower bounds for the quantifierfree fragment. 
16:30  An Introduction to the Clocked Lambda Calculus SPEAKER: unknown 
17:00  Work in Progress: Algebraic Abstract Reduction Systems SPEAKER: Benoît Valiron ABSTRACT. Several extensions of the lambdacalculus allow to rewrite a term into a linear combination of terms taking coefficients in the ring of nonnegative real numbers. The goal of this work is to define a notion of algebraic rewrite system abstracting away these calculi. In particular, we look for a notion of normalization induced by a rewriting compatible with the semiring structure and the usual topology on nonnegative reals. The goal is to achieve a kind of Newman's lemma: "strong normalization together with local confluence implies confluence". We state the formal definitions and show how a (naïve) expected implication fails short with several nontrivial examples. 
17:30  Turtle graphics of morphic streams SPEAKER: Hans Zantema 
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. 
16:30  On the Value of Variables SPEAKER: Beniamino Accattoli ABSTRACT. Callbyvalue and callbyneed lambdacalculi are defined using the 
17:00  Automated Complexity Analysis of Term Rewrite Systems SPEAKER: Martin Avanzini ABSTRACT. TcT, the Tyrolean complexity tool, is a tool for automatically proving 
17:30  Subrecursive Linear Dependent Types and Computational Security SPEAKER: Ugo Dal Lago ABSTRACT. Various techniques for the complexity analysis of programs have been introduced in the last twenty years, spanning from type systems, to abstract interpretation, to path orders. A peculiar approach consists in adopting linear dependent types, which have been proved to be a relative complete methodology for complexity analysis. We here study linear dependency in a subrecursive setting, where recursion is structural. On the one hand, we show that linear dependent types are robust enough to be adaptable, by way of effects, to a language with imperative features. On the other, we show the obtained system to be enough powerful to type nontrivial examples drawn from computational security, which is the driving motivation for this work. 
18:15  Proof theoretic approaches to rewriting SPEAKER: Thomas Powell ABSTRACT. A key method for establishing the termination or complexity of a 