View: session overviewtalk overviewside by side with other conferences

09:00 | Workshop introduction SPEAKER: David Baelde |

09:15 | An Introduction to Cyclic Proofs ABSTRACT. |

11:00 | Local Validity for Circular Proofs in Linear Logic with Fixed Points ABSTRACT. Circular (ie. non-wellfounded but regular) proofs received increasing interest in recent years with the simultaneous development of their applications and meta-theory: infinitary proof theory is now well-established in several proof-theoretical frameworks such as Martin Löf's inductive predicates, linear logic with fixed points, etc. In the setting of non-wellfounded proofs, a validity criterion is necessary to distinguish, among all infinite derivation trees (aka. pre-proofs), those which are logically valid proofs. A standard approach is to consider a pre-proof to be valid if every infinite branch is supported by a progressing thread. This work focuses on circular proofs for MALL with fixed points. Among all representations of valid circular proofs, a new fragment is described, based on a stronger validity criterion. This new criterion is based on a labelling of formulas and proofs, whose validity is purely local. This allows this fragment to be easily handled, while being expressive enough to still contain all circular embeddings of Baelde's muMALL finite proofs with (co)inductive invariants: in particular deciding validity and computing a certifying labelling can be done efficiently. Moreover the Brotherston-Simpson conjecture holds for this fragment: every labelled representation of a circular proof in the fragment is translated into a standard finitary proof. Finally we explore how to extend these results to a bigger fragment, by relaxing the labelling discipline while retaining (i) the ability to locally certify the validity and (ii) to some extent, the ability to finitize circular proofs. |

11:45 | SPEAKER: Florian Bruse ABSTRACT. Higher-Order Fixpoint Logic (HFL) is an extension of the modal mu-calculus by a typed lambda calculus. As in the mu-calculus, whether the nesting of least and greatest fixpoints increases expressive power is an important question. It is known that at low type theoretic levels, the fixpoint alternation hierarchy is strict. We present classes of structures over which the alternation hierarchy of HFL-formulas at low type level collapses into the alternation-free fragment, albeit at increase in type level by one. |

14:00 | Useless Explicit Induction Reasoning ABSTRACT. In the setting of classical first-order logic with inductive predicates, we give as example a theory for which the conjectures that cannot be proved without induction reasoning are still not provable by adding non-trivial explicit induction reasoning. |

14:45 | Towards the Automatic Construction of Schematic Proofs SPEAKER: David Cerna ABSTRACT. In recent years \emph{schematic representations} of proofs by induction have been studied for there interesting proof theoretic properties, i.e.\ allowing extensions of Herbrand's theorem to certain types of inductive proofs. Most of the work concerning these proof theoretic properties presented schematic proofs as sets of proofs connected by \emph{links} together with a global soundness condition. Recently, the $\mathcal{S}\mathit{i}\mathbf{LK}$-calculus was introduced which provides inferences for expanding the sets of proofs within a schematic proof as well as introducing links without violating the soundness condition. In this work we discuss a simplification of the $\mathcal{S}\mathit{i}\mathbf{LK}$-calculus which isolates the essential mechanisms and provides a path towards the automated construction of schematic proofs. |

16:00 | |

17:15 | SPEAKER: Patrick Bahr ABSTRACT. We give an overview of the syntax and semantics of Clocked Type Theory (CloTT), a dependent type theory for guarded recursion with many clocks, in which one can encode coinductive types and capture the notion of productivity in types. The main novelty of CloTT is the notion of ticks, which allows one to open the delay type modality, and, e.g., define a dependent form of applicative functor action, which can be used for reasoning about coinductive data. In the talk we will give examples of programming and reasoning about guarded recursive and coinductive data in CloTT, and we will present the main syntactic results: Strong normalisation, canonicity and decidability of type checking. If time permits, we will also sketch the main ideas of the denotational semantics for CloTT. |

Workshops dinner at Balliol College. Drinks reception from 7.45pm, to be seated by 8:15 (pre-booking via FLoC registration system required; guests welcome).