BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:Joost-Pieter Katoen (RWTH Aachen University)
DTSTART:20200415T130000Z
DTEND:20200415T140000Z
DTSTAMP:20260422T225659Z
UID:OWLS/1
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/OWLS/1/">Ter
 mination of probabilistic programs</a>\nby Joost-Pieter Katoen (RWTH Aache
 n University) as part of Online Worldwide Seminar on Logic and Semantics (
 OWLS)\n\n\nAbstract\nProgram termination is a key question in program veri
 fication. This talk considers the termination of probabilistic programs\, 
 programs that can describe randomised algorithms and more recently receive
 d attention in machine learning. Probabilistic termination has several nua
 nces and has some unexpected effects. Programs may diverge with zero proba
 bility\; they almost-surely terminate (AST). Two AST-programs run in seque
 nce may have an infinite expected run-time\, though each of its constituen
 ts has a finite expected run-time.\n\nThis talk will demystify the notions
  of probabilistic termination\, its surprising effects\, and its hardness 
 ("degree of undecidability"). We will show a simple proof rule for decidin
 g AST.\n
LOCATION:https://researchseminars.org/talk/OWLS/1/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Daniela Petrisan (University of Paris)
DTSTART:20200429T130000Z
DTEND:20200429T140000Z
DTSTAMP:20260422T225659Z
UID:OWLS/2
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/OWLS/2/">Com
 bining probabilistic and non-deterministic choice via weak distributive la
 ws</a>\nby Daniela Petrisan (University of Paris) as part of Online Worldw
 ide Seminar on Logic and Semantics (OWLS)\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/OWLS/2/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Bartek Klin (University of Warsaw)
DTSTART:20200513T130000Z
DTEND:20200513T140000Z
DTSTAMP:20260422T225659Z
UID:OWLS/3
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/OWLS/3/">Mon
 adic monadic second order logic</a>\nby Bartek Klin (University of Warsaw)
  as part of Online Worldwide Seminar on Logic and Semantics (OWLS)\n\n\nAb
 stract\nMonadic second order logic (MSO) is usually studied over specific 
 kinds of structures\, be it finite words\, infinite words\, finite or infi
 nite trees\, total orders of various shapes\, etc. A monad is a notion of 
 "a kind of structures" that covers these and many other examples. One can 
 formulate an abstract definition of MSO for a generic monad. I will explai
 n how this is done\, and I will describe some conditions that a monad shou
 ld satisfy to ensure a basic "sanity check": that every definable language
  is recognized by a finite algebra.\n\n(joint work with Mikołaj Bojańczy
 k and Julian Salamanca)\n
LOCATION:https://researchseminars.org/talk/OWLS/3/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Dexter Kozen (Cornell University)
DTSTART:20200527T130000Z
DTEND:20200527T140000Z
DTSTAMP:20260422T225659Z
UID:OWLS/4
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/OWLS/4/">Brz
 ozowski derivatives as distributive laws</a>\nby Dexter Kozen (Cornell Uni
 versity) as part of Online Worldwide Seminar on Logic and Semantics (OWLS)
 \n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/OWLS/4/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Valeria Vignudelli (ENS Lyon)
DTSTART:20200610T130000Z
DTEND:20200610T140000Z
DTSTAMP:20260422T225659Z
UID:OWLS/5
DESCRIPTION:by Valeria Vignudelli (ENS Lyon) as part of Online Worldwide S
 eminar on Logic and Semantics (OWLS)\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/OWLS/5/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Ryoma Sin'ya (Akita University)
DTSTART:20200930T140000Z
DTEND:20200930T150000Z
DTSTAMP:20260422T225659Z
UID:OWLS/6
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/OWLS/6/">Asy
 mptotic Approximation by Regular Languages (YR-OWLS)</a>\nby Ryoma Sin'ya 
 (Akita University) as part of Online Worldwide Seminar on Logic and Semant
 ics (OWLS)\n\n\nAbstract\nIn this talk we will introduce a new property of
  formal languages called REG-measurability where REG is the class of regul
 ar languages. Intuitively\, a language L is REG-measurable if there exists
  an infinite sequence of regular languages that ``converges'' to L. A lang
 uage without REG-measurability has a complex shape in some sense so that i
 t can not be approximated by regular languages.\n\nThe motivation\, why we
  have been interested in REG-measurability\, originally came from the foll
 owing conjecture posed by [Dömösi-Horvath-Ito 1991]: the set of all prim
 itive words over a non-singleton alphabet is not context-free.\n\nWe will 
 describe that several context-free languages are REG-measurable (including
  languages with transcendental generating function and transcendental dens
 ity\, in particular)\, while a certain simple deterministic context-free l
 anguage and the set of primitive words are REG-immeasurable in a strong se
 nse. We will also discuss some open problems and future work.\nThis talk i
 s based on the following work: http://www.math.akita-u.ac.jp/~ryoma/misc/m
 easure.pdf\n
LOCATION:https://researchseminars.org/talk/OWLS/6/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Andrej Bauer (University of Ljubljana)
DTSTART:20201007T140000Z
DTEND:20201007T150000Z
DTSTAMP:20260422T225659Z
UID:OWLS/7
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/OWLS/7/">Eff
 ects in the real world</a>\nby Andrej Bauer (University of Ljubljana) as p
 art of Online Worldwide Seminar on Logic and Semantics (OWLS)\n\n\nAbstrac
 t\nJoint work with Danel Ahman\, University of Ljubljana (https://danel.ah
 man.ee/).\n\nIn modern languages\, computational effects are often structu
 red using monads or algebraic effects and handlers. These mechanisms excel
  at implementation of computational effects within the language itself. Fo
 r instance\, the familiar implementation of mutable state in terms of stat
 e-passing functions requires no native state\, and can be implemented eith
 er as a monad or using handlers. One is naturally drawn to using these tec
 hniques also for dealing with actual effects\, such as manipulation of nat
 ive memory and access to hardware. These are represented inside the langua
 ge as algebraic operations or a monad\, but treated specially by the langu
 age's top-level runtime\, which invokes corresponding operating system fun
 ctionality. While this approach works in practice\, one wishes that the in
 genuity of the language implementors were better supported by a more flexi
 ble methodology with a sound theoretical footing.\n\nWe address the issue 
 by showing how to design a programming language based on runners of algebr
 aic effects. We review runners\, recast them as a programming construct\, 
 and present a calculus that captures the core ideas of programming with th
 em. Through examples of runners we show how they capture both the interact
 ion between the program and the external world\, and encapsulation of prog
 rams in virtual environments that tightly control access to external resou
 rces and provide strong guarantees of proper resource finalization.\n\nWe 
 accompanied our work with a prototype programming language Coop (https://g
 ithub.com/andrejbauer/coop) and a Haskell library for runners (https://git
 hub.com/danelahman/haskell-coop).\n\nReferences:\n\n - https://arxiv.org/a
 bs/1910.11629\n\n - https://github.com/andrejbauer/coop\n\n - https://gith
 ub.com/danelahman/haskell-coop\n
LOCATION:https://researchseminars.org/talk/OWLS/7/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Henning Basold (Universteit Leiden)
DTSTART:20201014T140000Z
DTEND:20201014T150000Z
DTSTAMP:20260422T225659Z
UID:OWLS/8
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/OWLS/8/">Coa
 lgebraic Communication Protocols and Session Types (YR-OWLS)</a>\nby Henni
 ng Basold (Universteit Leiden) as part of Online Worldwide Seminar on Logi
 c and Semantics (OWLS)\n\n\nAbstract\nThis is joint work with Alex Keizer 
 and Jorge A. Pérez.\n\nCompositional methods are central to the developme
 nt and verification of software systems. They allow to break down large sy
 stems into smaller components\, while enabling reasoning about the behavio
 ur of the composed system. For concurrent and communicating systems\, comp
 ositional techniques based on *behavioural type systems* have received muc
 h attention. By abstracting communication protocols as types\, these type 
 systems can statically check that programs interact with channels accordin
 g to a certain protocol\, whether the intended messages are exchanged in a
  certain order. For this talk\, we will put on our coalgebraic spectacles 
 to investigate *session types*\, a widely studied class of behavioral type
  systems. We will seek a syntax-free description of session-based concurre
 ncy as states of coalgebras. The result will be a description of type equi
 valence\, duality\, and subtyping relations in terms of canonical coinduct
 ive presentations. In turn\, this coinductive presentation makes it possib
 le to elegantly derive a decidable type system with subtyping for π-calcu
 lus processes\, in which the states of a coalgebra will serve as channel p
 rotocols. Going full circle\, we will also exhibit a coalgebra structure o
 n an existing session type system\, and show that the relations and type s
 ystem resulting from our coalgebraic perspective agree with the existing o
 nes.\n
LOCATION:https://researchseminars.org/talk/OWLS/8/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Antonin Kucera (Masaryk University)
DTSTART:20201021T140000Z
DTEND:20201021T150000Z
DTSTAMP:20260422T225659Z
UID:OWLS/9
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/OWLS/9/">Eff
 icient analysis of VASS termination complexity</a>\nby Antonin Kucera (Mas
 aryk University) as part of Online Worldwide Seminar on Logic and Semantic
 s (OWLS)\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/OWLS/9/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Sebastian Junges (UC Berkeley)
DTSTART:20201028T140000Z
DTEND:20201028T150000Z
DTSTAMP:20260422T225659Z
UID:OWLS/10
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/OWLS/10/">Fi
 nding Memoryless Policies in Partially Observable MDPs is ETR-complete (YR
 -OWLS)</a>\nby Sebastian Junges (UC Berkeley) as part of Online Worldwide 
 Seminar on Logic and Semantics (OWLS)\n\n\nAbstract\nPartially observable 
 Markov Decision Processes (POMDPs) are a prime model in sequential decisio
 n making. They are heavily studied in operations research\, artificial int
 elligence and verification\, to name a few. For POMDPs\, a good policy rea
 ches the target with probability at some threshold\, and makes its decisio
 ns solely based on the previously made observations. Deciding whether a go
 od policy exists is undecidable. One of the methods to solve instances of 
 this reachability problem is to restrict the memory that the strategy may 
 use. This approach is commonly taking\, e.g.\, in reinforcement learning f
 or POMDPs. In the first part of the talk\, we consider memoryless strategi
 es in POMDPs. and show that this problem is as hard as the feasibility pro
 blem in parametric Markov Chain (pMC) analysis.\n\nIn the second part of t
 he talk\, we consider this feasibility problem for pMCs. Roughly\, a pMC i
 s a Markov chain with symbolic transitions. The feasibility problem asks: 
 Do values for the symbols exist such that in the induced parameter-free Ma
 rkov chain\, a target state is reached with probability at least a half. W
 e discuss the complexity landscape for variants of this decision problem. 
 In particular\, we establish that feasibility in pMCs is complete for the 
 complexity class "existential theory of the reals” (ETR). Another exampl
 e of an ETR-complete problem is deciding whether a multivariate polynomial
  has a real root. Together with the results of the first half of the talk\
 , this establishes that deciding whether there exists a good memoryless po
 licy in a POMDP is ETR-complete.\n
LOCATION:https://researchseminars.org/talk/OWLS/10/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Orna Kupferman (Hebrew University)
DTSTART:20201104T140000Z
DTEND:20201104T150000Z
DTSTAMP:20260422T225659Z
UID:OWLS/11
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/OWLS/11/">Ex
 amining Classical Graph-Theory Problems from the Viewpoint of Formal-Verif
 ication Methods</a>\nby Orna Kupferman (Hebrew University) as part of Onli
 ne Worldwide Seminar on Logic and Semantics (OWLS)\n\n\nAbstract\nThe talk
  surveys a series of works that lift the rich semantics and structure of g
 raphs\, and the experience of the formal-verification community in reasoni
 ng about them\, to classical graph-theoretical problems.\n
LOCATION:https://researchseminars.org/talk/OWLS/11/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Joël Ouaknine (Max Planck Institute for Software Systems)
DTSTART:20201118T140000Z
DTEND:20201118T150000Z
DTSTAMP:20260422T225659Z
UID:OWLS/12
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/OWLS/12/">Ho
 lonomic Techniques\, Periods\, and Decision Problems</a>\nby Joël Ouaknin
 e (Max Planck Institute for Software Systems) as part of Online Worldwide 
 Seminar on Logic and Semantics (OWLS)\n\n\nAbstract\nHolonomic techniques 
 have deep roots going back to Wallis\, Euler\, and Gauss\, and have evolve
 d in modern times as an important subfield of computer algebra\, thanks in
  large part to the work of Zeilberger and others over the past three decad
 es. In this talk\, I will give an overview of the area\, and in particular
  will present a select survey of known and original results on decision pr
 oblems for holonomic sequences and functions. I will also discuss some sur
 prising connections to the theory of periods and exponential periods\, whi
 ch are classical objects of study in algebraic geometry and number theory\
 ; in particular\, I will relate the decidability of certain decision probl
 ems for holonomic sequences to deep conjectures about periods and exponent
 ial periods\, notably those due to Kontsevich and Zagier.\n\nParts of this
  talk will be based on the paper "On Positivity and Minimality for Second-
 Order Holonomic Sequences"\, https://arxiv.org/abs/2007.12282.\n
LOCATION:https://researchseminars.org/talk/OWLS/12/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Francesco Gavazzo (University of Bologna)
DTSTART:20201125T140000Z
DTEND:20201125T150000Z
DTSTAMP:20260422T225659Z
UID:OWLS/13
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/OWLS/13/">Mo
 dal Reasoning = Metric Reasoning\, via Lawvere (YR-OWLS)</a>\nby Francesco
  Gavazzo (University of Bologna) as part of Online Worldwide Seminar on Lo
 gic and Semantics (OWLS)\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/OWLS/13/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Derek Dreyer (Max Planck Institute for Software Systems)
DTSTART:20201209T140000Z
DTEND:20201209T150000Z
DTSTAMP:20260422T225659Z
UID:OWLS/14
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/OWLS/14/">Tu
 rning Iris Up to Eleven: Next Steps in Higher-Order Separation Logic</a>\n
 by Derek Dreyer (Max Planck Institute for Software Systems) as part of Onl
 ine Worldwide Seminar on Logic and Semantics (OWLS)\n\n\nAbstract\nIris is
  a framework for higher-order concurrent separation logic\, implemented in
  the Coq proof assistant\, which we have been developing since 2014. Origi
 nally designed for pedagogical purposes\, Iris has grown into a ongoing\, 
 multi-institution project\, with active collaborators at Aarhus University
 \, BedRock Systems\, Boston College\, CNRS/LRI\, Groningen University\, IN
 RIA\, ITU Copenhagen\, KU Leuven\, Microsoft Research\, MIT\, MPI-SWS\, NY
 U\, Radboud University Nijmegen\, Saarland University\, and Vrije Universi
 teit Brussel\, and over 35 published papers studying or deploying Iris for
  verification of complex programs and programming language meta-theory in 
 Rust\, Go\, OCaml\, Scala\, and more (https://iris-project.org).\n\nIn thi
 s talk\, we will present two brand new -- and very different -- developmen
 ts that have the potential to extend the reach of Iris even further. The f
 irst is a new *ownership-based refinement type system* for C\, which suppo
 rts *automated* verification of C programs while at the same time being *f
 oundational* (producing Iris proofs in Coq). The second is a complete "rem
 odeling" of Iris\, replacing its original step-indexed model with a *trans
 finite* step-indexed model in order to make Iris suitable for verification
  of liveness properties.\n\nFor this talk\, we will not assume any prior k
 nowledge of Iris. Rather\, we will briefly review the distinguishing featu
 res of Iris\, and then explain the key insights behind the aforementioned 
 new developments -- and the problems they are solving -- at a high level o
 f abstraction.\n\nThe first new development is joint work with Michael Sam
 mler\, Rodolphe Lepigre\, Robbert Krebbers\, Kayvan Memarian\, and Deepak 
 Garg. The second is joint work with Simon Spies\, Lennard Gäher\, Daniel 
 Gratzer\, Joseph Tassarotti\, Robbert Krebbers\, and Lars Birkedal.\n
LOCATION:https://researchseminars.org/talk/OWLS/14/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Maaike Zwart (University of Oxford)
DTSTART:20201202T140000Z
DTEND:20201202T150000Z
DTSTAMP:20260422T225659Z
UID:OWLS/15
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/OWLS/15/">Di
 stributive Laws in the Boom Hierarchy (YR-OWLS)</a>\nby Maaike Zwart (Univ
 ersity of Oxford) as part of Online Worldwide Seminar on Logic and Semanti
 cs (OWLS)\n\n\nAbstract\nDuring my PhD research I have studied distributiv
 e laws for monads\, and developed various no-go theorems. These theorems p
 rove that monads with certain algebraic properties cannot be composed with
  each other via a distributive law. In this talk I will focus on examples\
 , and share the intuition that I have developed from my results. All the e
 xamples in this talk will be based on the Boom hierarchy\, a hierarchy of 
 data structures which lends itself perfectly for the study of monad compos
 itions. Based on which monads in this hierarchy do and do not compose with
  each other via a distributive law\, I will make predictions about the beh
 aviour of monad compositions in general.\n
LOCATION:https://researchseminars.org/talk/OWLS/15/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Abhisekh Sankaran (University of Cambridge)
DTSTART:20201111T140000Z
DTEND:20201111T150000Z
DTSTAMP:20260422T225659Z
UID:OWLS/16
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/OWLS/16/">Ex
 tension preservation in the finite and prefix classes of first order logic
 </a>\nby Abhisekh Sankaran (University of Cambridge) as part of Online Wor
 ldwide Seminar on Logic and Semantics (OWLS)\n\n\nAbstract\nIt is well kno
 wn that the classic Łoś-Tarski preservation theorem fails in the finite:
  there are first-order definable classes of finite structures closed under
  extensions which are not definable (in the finite) in the existential fra
 gment of first-order logic. We strengthen this by constructing for every n
 \, first-order definable classes of finite structures closed under extensi
 ons which are not definable with n quantifier alternations. The classes we
  construct are definable in the extension of Datalog with negation and ind
 eed in the existential fragment of transitive-closure logic. This answers 
 negatively an open question posed by Rosen and Weinstein.\n
LOCATION:https://researchseminars.org/talk/OWLS/16/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Moshe Vardi (Rice University)
DTSTART:20201216T140000Z
DTEND:20201216T150000Z
DTSTAMP:20260422T225659Z
UID:OWLS/17
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/OWLS/17/">Le
 ssons from COVID-19: Efficiency vs Resilience</a>\nby Moshe Vardi (Rice Un
 iversity) as part of Online Worldwide Seminar on Logic and Semantics (OWLS
 )\n\n\nAbstract\nIn both computer science and economics\, efficiency is a 
 cherished property. In computer science\, the field of algorithms is almos
 t solely focused on their efficiency. In economics\, the main advantage of
  the free market is that it promises "economic efficiency." A major lesson
  from COVID-19 is that both fields have over-emphasized efficiency and und
 er-emphasized resilience. I argue that resilience is a more important prop
 erty than efficiency and discuss how the two fields can broaden their focu
 s to make resilience a primary consideration. I will include a technical e
 xample\, showing how we can shift the focus in strategic reasoning from ef
 ficiency to resilience.\n
LOCATION:https://researchseminars.org/talk/OWLS/17/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Sarah Winter (Université libre de Bruxelles)
DTSTART:20210106T140000Z
DTEND:20210106T150000Z
DTSTAMP:20260422T225659Z
UID:OWLS/18
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/OWLS/18/">Sy
 nthesizing computable functions from synchronous specifications</a>\nby Sa
 rah Winter (Université libre de Bruxelles) as part of Online Worldwide Se
 minar on Logic and Semantics (OWLS)\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/OWLS/18/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Ori Lahav (School of Computer Science at Tel Aviv University)
DTSTART:20210120T140000Z
DTEND:20210120T150000Z
DTSTAMP:20260422T225659Z
UID:OWLS/19
DESCRIPTION:by Ori Lahav (School of Computer Science at Tel Aviv Universit
 y) as part of Online Worldwide Seminar on Logic and Semantics (OWLS)\n\nAb
 stract: TBA\n
LOCATION:https://researchseminars.org/talk/OWLS/19/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Sonia Marin (University College London)
DTSTART:20210203T140000Z
DTEND:20210203T150000Z
DTSTAMP:20260422T225659Z
UID:OWLS/20
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/OWLS/20/">Fr
 om axioms to synthetic inference rules via focusing</a>\nby Sonia Marin (U
 niversity College London) as part of Online Worldwide Seminar on Logic and
  Semantics (OWLS)\n\n\nAbstract\nFocusing is a general technique that was 
 designed to improve proof search\, but has since become increasingly relev
 ant in structural proof theory. The essential idea is to identify and merg
 e the non-deterministic choices in a proof. A focused proof is then given 
 by the alternation of phases where invertible rules are applied eagerly (b
 ottom-up) and phases where the other rules are confined and controlled. Th
 e focusing theorem\, which asserts the completeness of focused proofs\, de
 livers strong representational benefits. For instance\, by ignoring the in
 ternal structure of the phases one obtains a well-behaved notion of ‘syn
 thetic rule’ (e.g. they commute with cut-reduction steps). In this talk\
 , we will present a careful study of a family of synthetic rules\, the bip
 oles\, giving a fresh view to an old problem: how to incorporate inference
  rules corresponding to axioms into proof systems for classical and intuit
 ionistic logics. As different synthetic inference rules can be produced fo
 r the same axiom\, we in fact unify and generalise previous approaches for
  transforming axioms into rules. This is joint work with Dale Miller\, Ela
 ine Pimentel\, and Marco Volpe.\n
LOCATION:https://researchseminars.org/talk/OWLS/20/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Benjamin Kaminski (University College London)
DTSTART:20210217T140000Z
DTEND:20210217T150000Z
DTSTAMP:20260422T225659Z
UID:OWLS/21
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/OWLS/21/">Qu
 antitative Separation Logic</a>\nby Benjamin Kaminski (University College 
 London) as part of Online Worldwide Seminar on Logic and Semantics (OWLS)\
 n\n\nAbstract\nWe present quantitative separation logic (QSL). In contrast
  to classical separation logic\, QSL employs quantities which evaluate to 
 real numbers instead of predicates which evaluate to Boolean values. The c
 onnectives of classical separation logic\, separating conjunction and sepa
 rating implication\, are lifted from predicates to quantities. This extens
 ion is conservative: Both connectives are backward compatible to their cla
 ssical analogs and obey the same laws\, e.g. modus ponens\, adjointness\, 
 etc. Furthermore\, we present a weakest precondition calculus for quantita
 tive reasoning about probabilistic pointer programs in QSL. This calculus 
 is a conservative extension of both Ishtiaq's\, O'Hearn's and Reynolds' se
 paration logic for heap-manipulating programs and Kozen's / McIver and Mor
 gan's weakest preexpectations for probabilistic programs. Our calculus pre
 serves O'Hearn's frame rule\, which enables local reasoning - a key princi
 ple of separation logic. Finally\, we briefly touch upon open questions re
 garding lower bounds on weakest preexpectations and intensional completene
 ss of our calculus.\n
LOCATION:https://researchseminars.org/talk/OWLS/21/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Tiziano Dalmonte (TU Wien)
DTSTART:20210331T140000Z
DTEND:20210331T150000Z
DTSTAMP:20260422T225659Z
UID:OWLS/22
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/OWLS/22/">Pr
 oof systems and countermodels for non-normal modal logics</a>\nby Tiziano 
 Dalmonte (TU Wien) as part of Online Worldwide Seminar on Logic and Semant
 ics (OWLS)\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/OWLS/22/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Jorge Perez (University of Groningen)
DTSTART:20210224T140000Z
DTEND:20210224T150000Z
DTSTAMP:20260422T225659Z
UID:OWLS/23
DESCRIPTION:by Jorge Perez (University of Groningen) as part of Online Wor
 ldwide Seminar on Logic and Semantics (OWLS)\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/OWLS/23/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Dale Miller (Inria and LIX\, Ecole Polytechnique)
DTSTART:20210310T140000Z
DTEND:20210310T150000Z
DTSTAMP:20260422T225659Z
UID:OWLS/24
DESCRIPTION:by Dale Miller (Inria and LIX\, Ecole Polytechnique) as part o
 f Online Worldwide Seminar on Logic and Semantics (OWLS)\n\nAbstract: TBA\
 n
LOCATION:https://researchseminars.org/talk/OWLS/24/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Anca Muscholl (Université Bordeaux)
DTSTART:20210324T140000Z
DTEND:20210324T150000Z
DTSTAMP:20260422T225659Z
UID:OWLS/25
DESCRIPTION:by Anca Muscholl (Université Bordeaux) as part of Online Worl
 dwide Seminar on Logic and Semantics (OWLS)\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/OWLS/25/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Assia Mahboubi (Inria and Vrije Universiteit Amsterdam)
DTSTART:20210407T140000Z
DTEND:20210407T150000Z
DTSTAMP:20260422T225659Z
UID:OWLS/26
DESCRIPTION:by Assia Mahboubi (Inria and Vrije Universiteit Amsterdam) as 
 part of Online Worldwide Seminar on Logic and Semantics (OWLS)\n\nAbstract
 : TBA\n
LOCATION:https://researchseminars.org/talk/OWLS/26/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Alessio Guglielmi (University of Bath)
DTSTART:20210505T140000Z
DTEND:20210505T150000Z
DTSTAMP:20260422T225659Z
UID:OWLS/27
DESCRIPTION:by Alessio Guglielmi (University of Bath) as part of Online Wo
 rldwide Seminar on Logic and Semantics (OWLS)\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/OWLS/27/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Pierre Ohlmann (Université de Paris)
DTSTART:20210317T140000Z
DTEND:20210317T150000Z
DTSTAMP:20260422T225659Z
UID:OWLS/28
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/OWLS/28/">Co
 ntrolling a random population</a>\nby Pierre Ohlmann (Université de Paris
 ) as part of Online Worldwide Seminar on Logic and Semantics (OWLS)\n\nAbs
 tract: TBA\n
LOCATION:https://researchseminars.org/talk/OWLS/28/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Joshua Moerman (RWTH Aachen)
DTSTART:20210414T140000Z
DTEND:20210414T150000Z
DTSTAMP:20260422T225659Z
UID:OWLS/29
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/OWLS/29/">We
 ighted Register Automata</a>\nby Joshua Moerman (RWTH Aachen) as part of O
 nline Worldwide Seminar on Logic and Semantics (OWLS)\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/OWLS/29/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Andy Pitts (Cambridge)
DTSTART:20210421T140000Z
DTEND:20210421T150000Z
DTSTAMP:20260422T225659Z
UID:OWLS/30
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/OWLS/30/">Co
 nstructive Initial Algebra Semantics</a>\nby Andy Pitts (Cambridge) as par
 t of Online Worldwide Seminar on Logic and Semantics (OWLS)\n\nAbstract: T
 BA\n
LOCATION:https://researchseminars.org/talk/OWLS/30/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Fabio Zanasi (UCL London)
DTSTART:20210428T140000Z
DTEND:20210428T150000Z
DTSTAMP:20260422T225659Z
UID:OWLS/31
DESCRIPTION:by Fabio Zanasi (UCL London) as part of Online Worldwide Semin
 ar on Logic and Semantics (OWLS)\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/OWLS/31/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Masaki Waga (Kyoto University)
DTSTART:20210512T140000Z
DTEND:20210512T150000Z
DTSTAMP:20260422T225659Z
UID:OWLS/32
DESCRIPTION:by Masaki Waga (Kyoto University) as part of Online Worldwide 
 Seminar on Logic and Semantics (OWLS)\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/OWLS/32/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Gabriel Scherer (INRIA)
DTSTART:20210526T140000Z
DTEND:20210526T150000Z
DTSTAMP:20260422T225659Z
UID:OWLS/33
DESCRIPTION:by Gabriel Scherer (INRIA) as part of Online Worldwide Seminar
  on Logic and Semantics (OWLS)\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/OWLS/33/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Adwait Godbole (University of California at Berkeley)
DTSTART:20210609T140000Z
DTEND:20210609T150000Z
DTSTAMP:20260422T225659Z
UID:OWLS/34
DESCRIPTION:by Adwait Godbole (University of California at Berkeley) as pa
 rt of Online Worldwide Seminar on Logic and Semantics (OWLS)\n\nAbstract: 
 TBA\n
LOCATION:https://researchseminars.org/talk/OWLS/34/
END:VEVENT
END:VCALENDAR