CSL 2022

Invited Speakers

• 

  Tuesday: 10:00 - 11:00

  On the existence of sequent calculi

  Proof systems are often used to prove that a logic has certain properties, such as decidability or interpolation. Depending on the property, one proof system can be more useful than another in this respect. Sequent calculi are popular proof systems for all kinds of applications. Usually the effectiveness of a sequent calculus comes from the good structural properties that it has. This leads to the question which logics do have good sequent calculi and which do not. In this talk a method to prove negative results of this kind, i.e.~results establishing that a logic does not have certain good calculi, is presented. It makes use of a logical property, uniform interpolation, that is a strengthening of interpolation that is rare in some classes of logics. When applied to modal, intermediate, substructural or intuitionistic modal logics, the method implies that those logics without uniform interpolation do not have sequent calculi with certain good structural properties. On the other hand, the method also provides a general technique to prove that certain logics in these classes do have uniform interpolation. As an example it is shown that Lax Logic, a logic with applications in a number of areas, ranging from algebraic logic to hardware verification, has uniform interpolation.

  Rosalie Iemhoff

  Rosalie Iemhoff is a professor at Utrecht University, the Netherlands, specializing in mathematical and philosophical logic, with a special interest in proof theory, its aims and its methods. Rosalie studied mathematics at the University of Amsterdam, and obtained a PhD in mathematical logic at the same university in 2001. After spending several years as a postdoc, at the University of California, San Diego, and the Technical University Vienna, she joined the Department of Philosophy at Utrecht University in 2006. In 2018 she received a large grant for a five year research project Optimal Proofs on the proof theory of logics. Rosalie is one of the editor’s in chief of the Journal of Philosophical Logic.

• 

  Wednesday 14:00 - 15:00

  Between Deterministic and Nondeterministic Quantitative Automata

  There is a challenging trade-off between deterministic and nondeterministic automata, where the former suit various applications better, however at the cost of being exponentially larger or even less expressive. This gave birth to many notions in between determinism and nondeterminism, aiming at enjoying, sometimes, the best of both worlds. We analyze the possible generalization of such notions from Boolean to quantitative automata, and suggest that it depends on the following key characteristics of the considered notion---whether it is syntactic or semantic, and if semantic, whether it is word-based or language-based. We classify numerous notions known in the Boolean setting according to their characterization above, generalize them to the quantitative setting and look into relations between them. The generalized notions open new research directions with respect to quantitative automata, and provide insights on the original notions with respect to Boolean automata.

  Udi Boker

  Udi Boker is Professor of Computer Science at the Interdisciplinary Center (IDC) Herzliya, Israel. He specializes in logic, formal verification, computational models, game theory, and automata theory. He received his PhD in computer science from the Tel-Aviv University, and did postdoctoral research in the Hebrew University and in the Institute of Science and Technology (IST) Austria. Prior to joining the academy, he served as an R&D Director in the Hi-Tech company Mercury Interactive, initiating and leading the area of load-testing over the Internet.

• 

  Thursday: 14:00 - 15:00

  Classification in computable structure theory

  In computable structure theory, one studies the computational content of particular encodings of structures. Given a family of structures (such as finite branching trees or free groups), it is natural to want to classify those in the family that are computable. Here we provide a self-contained overview of approaches to classification in this field and explore results about families of structures such as those above.

  Karen Lange

  Karen Lange is an associate professor of mathematics at Wellesley College. Her research is in computability theory; she studies the ''balance scales'' used to calibrate computational information and applies these tools to measure the difficulty of algebraic problems. She earned her undergraduate degree at Swarthmore College and her doctoral degree at the University of Chicago, and she completed an NSF Postdoctoral Fellowship at the University of Notre Dame.

• 

  Friday: 10:00 - 11:00

  How to develop an intuition for risk. . . and other invisible phenomena

  The study of quantitative risk in security systems is often based around complex and subtle mathematical ideas involving probabilities. The notations for these ideas can pose a communication barrier between collaborating researchers even when those researchers are working within a similar framework. In this talk I will describe the use of geometrical representation and reasoning as a way to share ideas using the minimum of (formal) notation so as to build intuition about what kinds of properties might or might not be true. I will describe a faithful geometrical setting for the channel model of quantitative information flow (QIF) and demonstrate how it can facilitate “proofs without words” for problems in the QIF setting.

  Annabelle McIver

  Annabelle McIver is a professor of Computer Science at Macquarie University in Sydney. Annabelle trained as a mathematician at Cambridge and Oxford Universities. Her research uses mathematics to prove quantitative properties of programs, and more recently to provide foundations for quantitative information flow for analysing security properties. She is co-author of the book ''Abstraction, Refinement and Proof for Probabilistic Systems'', and ''The Science of Quantitative Information Flow''.

• 

  Saturday: 11:30 - 12:30

  Seemingly impossible programs and proofs

  In previous work we developed algorithms that perform the seemingly impossible task of exhaustively searching infinite sets in finite time. To formulate and prove their correctness, we used a combination of programming language semantics, topology and higher-type computability theory. In this talk, we explore the same ideas from a different, logical angle. The algorithms are derived from constructive proofs of instances of the law of the excluded middle that, at first sight, look constructively implausible. To achieve this, we work in dependent type theory, a foundation for constructive mathematics that can also be considered as a programming language. Familiarity with type theory will not be assumed.

  Martin Escardo

  Martín Escardó is a Professor of Theoretical Computer Science at the School of Computer Science of the University of Birmingham, UK. His research interests include topology, locale theory, domain theory, game theory, homotopy type theory, formalization of mathematics, constructive mathematics. He studied at UFRGS, Brazil, and received a PhD from Imperial College, London. Before joining Birmingham, he was a lecturer at the universities of Edinburgh and St Andrews in Scotland.