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;VALUE=DATE-TIME:20200415T130000Z
DTEND;VALUE=DATE-TIME:20200415T140000Z
DTSTAMP;VALUE=DATE-TIME:20240329T101311Z
UID:OWLS/1
DESCRIPTION:Title: Ter
mination of probabilistic programs\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;VALUE=DATE-TIME:20200429T130000Z
DTEND;VALUE=DATE-TIME:20200429T140000Z
DTSTAMP;VALUE=DATE-TIME:20240329T101311Z
UID:OWLS/2
DESCRIPTION:Title: Com
bining probabilistic and non-deterministic choice via weak distributive la
ws\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;VALUE=DATE-TIME:20200513T130000Z
DTEND;VALUE=DATE-TIME:20200513T140000Z
DTSTAMP;VALUE=DATE-TIME:20240329T101311Z
UID:OWLS/3
DESCRIPTION:Title: Mon
adic monadic second order logic\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;VALUE=DATE-TIME:20200527T130000Z
DTEND;VALUE=DATE-TIME:20200527T140000Z
DTSTAMP;VALUE=DATE-TIME:20240329T101311Z
UID:OWLS/4
DESCRIPTION:Title: Brz
ozowski derivatives as distributive laws\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;VALUE=DATE-TIME:20200610T130000Z
DTEND;VALUE=DATE-TIME:20200610T140000Z
DTSTAMP;VALUE=DATE-TIME:20240329T101311Z
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;VALUE=DATE-TIME:20200930T140000Z
DTEND;VALUE=DATE-TIME:20200930T150000Z
DTSTAMP;VALUE=DATE-TIME:20240329T101311Z
UID:OWLS/6
DESCRIPTION:Title: Asy
mptotic Approximation by Regular Languages (YR-OWLS)\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;VALUE=DATE-TIME:20201007T140000Z
DTEND;VALUE=DATE-TIME:20201007T150000Z
DTSTAMP;VALUE=DATE-TIME:20240329T101311Z
UID:OWLS/7
DESCRIPTION:Title: Eff
ects in the real world\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;VALUE=DATE-TIME:20201014T140000Z
DTEND;VALUE=DATE-TIME:20201014T150000Z
DTSTAMP;VALUE=DATE-TIME:20240329T101311Z
UID:OWLS/8
DESCRIPTION:Title: Coa
lgebraic Communication Protocols and Session Types (YR-OWLS)\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;VALUE=DATE-TIME:20201021T140000Z
DTEND;VALUE=DATE-TIME:20201021T150000Z
DTSTAMP;VALUE=DATE-TIME:20240329T101311Z
UID:OWLS/9
DESCRIPTION:Title: Eff
icient analysis of VASS termination complexity\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;VALUE=DATE-TIME:20201028T140000Z
DTEND;VALUE=DATE-TIME:20201028T150000Z
DTSTAMP;VALUE=DATE-TIME:20240329T101311Z
UID:OWLS/10
DESCRIPTION:Title: Fi
nding Memoryless Policies in Partially Observable MDPs is ETR-complete (YR
-OWLS)\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;VALUE=DATE-TIME:20201104T140000Z
DTEND;VALUE=DATE-TIME:20201104T150000Z
DTSTAMP;VALUE=DATE-TIME:20240329T101311Z
UID:OWLS/11
DESCRIPTION:Title: Ex
amining Classical Graph-Theory Problems from the Viewpoint of Formal-Verif
ication Methods\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;VALUE=DATE-TIME:20201118T140000Z
DTEND;VALUE=DATE-TIME:20201118T150000Z
DTSTAMP;VALUE=DATE-TIME:20240329T101311Z
UID:OWLS/12
DESCRIPTION:Title: Ho
lonomic Techniques\, Periods\, and Decision Problems\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;VALUE=DATE-TIME:20201125T140000Z
DTEND;VALUE=DATE-TIME:20201125T150000Z
DTSTAMP;VALUE=DATE-TIME:20240329T101311Z
UID:OWLS/13
DESCRIPTION:Title: Mo
dal Reasoning = Metric Reasoning\, via Lawvere (YR-OWLS)\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;VALUE=DATE-TIME:20201209T140000Z
DTEND;VALUE=DATE-TIME:20201209T150000Z
DTSTAMP;VALUE=DATE-TIME:20240329T101311Z
UID:OWLS/14
DESCRIPTION:Title: Tu
rning Iris Up to Eleven: Next Steps in Higher-Order Separation Logic\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;VALUE=DATE-TIME:20201202T140000Z
DTEND;VALUE=DATE-TIME:20201202T150000Z
DTSTAMP;VALUE=DATE-TIME:20240329T101311Z
UID:OWLS/15
DESCRIPTION:Title: Di
stributive Laws in the Boom Hierarchy (YR-OWLS)\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;VALUE=DATE-TIME:20201111T140000Z
DTEND;VALUE=DATE-TIME:20201111T150000Z
DTSTAMP;VALUE=DATE-TIME:20240329T101311Z
UID:OWLS/16
DESCRIPTION:Title: Ex
tension preservation in the finite and prefix classes of first order logic
\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;VALUE=DATE-TIME:20201216T140000Z
DTEND;VALUE=DATE-TIME:20201216T150000Z
DTSTAMP;VALUE=DATE-TIME:20240329T101311Z
UID:OWLS/17
DESCRIPTION:Title: Le
ssons from COVID-19: Efficiency vs Resilience\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;VALUE=DATE-TIME:20210106T140000Z
DTEND;VALUE=DATE-TIME:20210106T150000Z
DTSTAMP;VALUE=DATE-TIME:20240329T101311Z
UID:OWLS/18
DESCRIPTION:Title: Sy
nthesizing computable functions from synchronous specifications\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;VALUE=DATE-TIME:20210120T140000Z
DTEND;VALUE=DATE-TIME:20210120T150000Z
DTSTAMP;VALUE=DATE-TIME:20240329T101311Z
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;VALUE=DATE-TIME:20210203T140000Z
DTEND;VALUE=DATE-TIME:20210203T150000Z
DTSTAMP;VALUE=DATE-TIME:20240329T101311Z
UID:OWLS/20
DESCRIPTION:Title: Fr
om axioms to synthetic inference rules via focusing\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;VALUE=DATE-TIME:20210217T140000Z
DTEND;VALUE=DATE-TIME:20210217T150000Z
DTSTAMP;VALUE=DATE-TIME:20240329T101311Z
UID:OWLS/21
DESCRIPTION:Title: Qu
antitative Separation Logic\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;VALUE=DATE-TIME:20210331T140000Z
DTEND;VALUE=DATE-TIME:20210331T150000Z
DTSTAMP;VALUE=DATE-TIME:20240329T101311Z
UID:OWLS/22
DESCRIPTION:Title: Pr
oof systems and countermodels for non-normal modal logics\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;VALUE=DATE-TIME:20210224T140000Z
DTEND;VALUE=DATE-TIME:20210224T150000Z
DTSTAMP;VALUE=DATE-TIME:20240329T101311Z
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;VALUE=DATE-TIME:20210310T140000Z
DTEND;VALUE=DATE-TIME:20210310T150000Z
DTSTAMP;VALUE=DATE-TIME:20240329T101311Z
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;VALUE=DATE-TIME:20210324T140000Z
DTEND;VALUE=DATE-TIME:20210324T150000Z
DTSTAMP;VALUE=DATE-TIME:20240329T101311Z
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;VALUE=DATE-TIME:20210407T140000Z
DTEND;VALUE=DATE-TIME:20210407T150000Z
DTSTAMP;VALUE=DATE-TIME:20240329T101311Z
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;VALUE=DATE-TIME:20210505T140000Z
DTEND;VALUE=DATE-TIME:20210505T150000Z
DTSTAMP;VALUE=DATE-TIME:20240329T101311Z
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;VALUE=DATE-TIME:20210317T140000Z
DTEND;VALUE=DATE-TIME:20210317T150000Z
DTSTAMP;VALUE=DATE-TIME:20240329T101311Z
UID:OWLS/28
DESCRIPTION:Title: Co
ntrolling a random population\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;VALUE=DATE-TIME:20210414T140000Z
DTEND;VALUE=DATE-TIME:20210414T150000Z
DTSTAMP;VALUE=DATE-TIME:20240329T101311Z
UID:OWLS/29
DESCRIPTION:Title: We
ighted Register Automata\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;VALUE=DATE-TIME:20210421T140000Z
DTEND;VALUE=DATE-TIME:20210421T150000Z
DTSTAMP;VALUE=DATE-TIME:20240329T101311Z
UID:OWLS/30
DESCRIPTION:Title: Co
nstructive Initial Algebra Semantics\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;VALUE=DATE-TIME:20210428T140000Z
DTEND;VALUE=DATE-TIME:20210428T150000Z
DTSTAMP;VALUE=DATE-TIME:20240329T101311Z
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;VALUE=DATE-TIME:20210512T140000Z
DTEND;VALUE=DATE-TIME:20210512T150000Z
DTSTAMP;VALUE=DATE-TIME:20240329T101311Z
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;VALUE=DATE-TIME:20210526T140000Z
DTEND;VALUE=DATE-TIME:20210526T150000Z
DTSTAMP;VALUE=DATE-TIME:20240329T101311Z
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;VALUE=DATE-TIME:20210609T140000Z
DTEND;VALUE=DATE-TIME:20210609T150000Z
DTSTAMP;VALUE=DATE-TIME:20240329T101311Z
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