
For a regular cardinal $\kappa$, a formula of the modal $\mu$calculus is
$\kappa$continuous in a variable x if, on every model, its interpretation as a
unary function of x is monotone and preserves unions of $\kappa$directed sets.
We define the fragment $C_{\aleph_1}(x)$ of the modal $\mu$calculus and prove
that all the formulas in this fragment are $\aleph_1$continuous. For each
formula $\phi(x)$ of the modal $\mu$calculus, we construct a formula $\psi(x)
\in C_{\aleph_1 }(x)$ such that $\phi(x)$ is $\kappa$continuous, for some
$\kappa$, if and only if $\phi(x)$ is equivalent to $\psi(x)$. Consequently, we
prove that (i) the problem whether a formula is $\kappa$continuous for some
$\kappa$ is decidable, (ii) up to equivalence, there are only two fragments
determined by continuity at some regular cardinal: the fragment
$C_{\aleph_0}(x)$ studied by Fontaine and the fragment $C_{\aleph_1}(x)$. We
apply our considerations to the problem of characterizing closure ordinals of
formulas of the modal $\mu$calculus. An ordinal $\alpha$ is the closure
ordinal of a formula $\phi(x)$ if its interpretation on every model converges
to its least fixedpoint in at most $\alpha$ steps and if there is a model
where the convergence occurs exactly in $\alpha$ steps. We prove that
$\omega_1$, the least uncountable ordinal, is such a closure ordinal. Moreover
we prove that closure ordinals are closed under ordinal sum. Thus, any formal
expression built from 0, 1, $\omega$, $\omega_1$ by using the binary operator
symbol + gives rise to a closure ordinal.

We introduce a parametrized version of the Wadge game for functions and show
that each lower cone in the Weihrauch degrees is characterized by such a game.
These parametrized Wadge games subsume the original Wadge game, the eraser and
backtrack games as well as Semmes's tree games. In particular, we propose that
the lower cones in the Weihrauch degrees are the answer to Andretta's question
on which classes of functions admit game characterizations.
We then discuss some applications of such parametrized Wadge games. Using
machinery from Weihrauch reducibility theory, we introduce games characterizing
every (transfinite) level of the Baire hierarchy via an iteration of a pruning
derivative on countably branching trees.

We investigate powerspace constructions on topological spaces, with a
particular focus on the category of quasiPolish spaces. We show that the upper
and lower powerspaces commute on all quasiPolish spaces, and show more
generally that this commutativity is equivalent to the topological property of
consonance. We then investigate powerspace constructions on the open set
lattices of quasiPolish spaces, and provide a complete characterization of how
the upper and lower powerspaces distribute over the open set lattice
construction.

Our concern is the completeness problem for spilogics, that is, sets of
implications between strictly positive formulas built from propositional
variables, conjunction and modal diamond operators. Originated in logic,
algebra and computer science, spilogics have two natural semantics:
meetsemilattices with monotone operators providing Birkhoffstyle calculi, and
firstorder relational structures (aka Kripke frames) often used as the
intended structures in applications. Here we lay foundations for a completeness
theory that aims to answer the question whether the two semantics define the
same consequence relations for a given spilogic.

Univalent homotopy type theory (HoTT) may be seen as a language for the
category of $\infty$groupoids. It is being developed as a new foundation for
mathematics and as an internal language for (elementary) higher toposes. We
develop the theory of factorization systems, reflective subuniverses, and
modalities in homotopy type theory, including their construction using a
"localization" higher inductive type. This produces in particular the
($n$connected, $n$truncated) factorization system as well as internal
presentations of subtoposes, through lex modalities. We also develop the
semantics of these constructions.

Recently, J. D. Lawson encouraged the domain theory community to consider the
scientific program of developing domain theory in the wider context of $T_0$
spaces instead of restricting to posets. In this paper, we respond to this
calling with an attempt to formulate a topological version of the Scott
Convergence Theorem, i.e., an ordertheoretic characterisation of those posets
for which the Scottconvergence $\mathcal{S}$ is topological. To do this, we
make use of the $\mathcal{ID}$ replacement principle to create topological
analogues of wellknown domaintheoretic concepts, e.g.,
$\mathcal{I}$continuous spaces correspond to continuous posets, as
$\mathcal{I}$convergence corresponds to $\mathcal{S}$convergence. In this
paper, we consider two novel topological concepts, namely, the
$\mathcal{I}$stable spaces and the $\mathcal{DI}$ spaces, and as a result we
obtain some necessary (respectively, sufficient) conditions under which the
convergence structure $\mathcal{I}$ is topological.

It has been known since Ehrhard and Regnier's seminal work on the Taylor
expansion of $\lambda$terms that this operation commutes with normalization:
the expansion of a $\lambda$term is always normalizable and its normal form is
the expansion of the B\"ohm tree of the term. We generalize this result to the
nonuniform setting of the algebraic $\lambda$calculus, i.e.
$\lambda$calculus extended with linear combinations of terms. This requires us
to tackle two difficulties: foremost is the fact that Ehrhard and Regnier's
techniques rely heavily on the uniform, deterministic nature of the ordinary
$\lambda$calculus, and thus cannot be adapted; second is the absence of any
satisfactory generic extension of the notion of B\"ohm tree in presence of
quantitative nondeterminism, which is reflected by the fact that the Taylor
expansion of an algebraic $\lambda$term is not always normalizable. Our
solution is to provide a fine grained study of the dynamics of
$\beta$reduction under Taylor expansion, by introducing a notion of reduction
on resource vectors, i.e. infinite linear combinations of resource
$\lambda$terms. The latter form the multilinear fragment of the differential
$\lambda$calculus, and resource vectors are the target of the Taylor expansion
of $\lambda$terms. We show the reduction of resource vectors contains the
image of any $\beta$reduction step, from which we deduce that Taylor expansion
and normalization commute on the nose. We moreover identify a class of
algebraic $\lambda$terms, encompassing both normalizable algebraic
$\lambda$terms and arbitrary ordinary $\lambda$terms: the expansion of these
is always normalizable, which guides the definition of a generalization of
B\"ohm trees to this setting.

We give an algebraic characterization of the syntax and operational semantics
of a class of simplytyped languages, such as the language PCF: we characterize
simplytyped syntax with variable binding and equipped with reduction rules via
a universal property, namely as the initial object of some category of models.
For this purpose, we employ techniques developed in two previous works: in the
first work we model syntactic translations between languages over different
sets of types as initial morphisms in a category of models. In the second work
we characterize untyped syntax with reduction rules as initial object in a
category of models. In the present work, we combine the techniques used earlier
in order to characterize simplytyped syntax with reduction rules as initial
object in a category. The universal property yields an operator which allows to
specify translationsthat are semantically faithful by constructionbetween
languages over possibly different sets of types.
As an example, we upgrade a translation from PCF to the untyped lambda
calculus, given in previous work, to account for reduction in the source and
target. Specifically, we specify a reduction semantics in the source and target
language through suitable rules. By equipping the untyped lambda calculus with
the structure of a model of PCF, initiality yields a translation from PCF to
the lambda calculus, that is faithful with respect to the reduction semantics
specified by the rules.
This paper is an extended version of an article published in the proceedings
of WoLLIC 2012.

We consider previous models of Timed, Probabilistic and Stochastic Timed
Automata, we introduce our model of Timed Automata with Polynomial Delay and we
characterize the expressiveness of these models relative to each other.

Automata expressiveness is an essential feature in understanding which of the
formalisms available should be chosen for modelling a particular problem.
Probabilistic and stochastic automata are suitable for modelling systems
exhibiting probabilistic behavior and their expressiveness has been studied
relative to nonprobabilistic transition systems and Markov chains. In this
paper, we consider previous formalisms of Timed, Probabilistic and Stochastic
Timed Automata, we present our new model of Timed Automata with Polynomial
Delay, we introduce a measure of expressiveness for automata we call trace
expressiveness and we characterize the expressiveness of these models relative
to each other under this new measure.

LP$^{\supset,\mathsf{F}}$ is a threevalued paraconsistent propositional
logic which is essentially the same as J3. It has most properties that have
been proposed as desirable properties of a reasonable paraconsistent
propositional logic. However, it follows easily from already published results
that there are exactly 8192 different threevalued paraconsistent propositional
logics that have the properties concerned. In this paper, properties concerning
the logical equivalence relation of a logic are used to distinguish
LP$^{\supset,\mathsf{F}}$ from the others. As one of the bonuses of focussing
on the logical equivalence relation, it is found that only 32 of the 8192
logics have a logical equivalence relation that satisfies the identity,
annihilation, idempotent, and commutative laws for conjunction and disjunction.
For most properties of LP$^{\supset,\mathsf{F}}$ that have been proposed as
desirable properties of a reasonable paraconsistent propositional logic, its
paracomplete analogue has a comparable property. In this paper, properties
concerning the logical equivalence relation of a logic are also used to
distinguish the paracomplete analogue of LP$^{\supset,\mathsf{F}}$ from the
other threevalued paracomplete propositional logics with those comparable
properties.

Stonetype duality theorems, which relate algebraic and
relational/topological models, are important tools in logic because  in
addition to elegant abstraction  they strengthen soundness and completeness
to a categorical equivalence, yielding a framework through which both algebraic
and topological methods can be brought to bear on a logic. We give a systematic
treatment of Stonetype duality for the structures that interpret bunched
logics, starting with the weakest systems, recovering the familiar BI and
Boolean BI (BBI), and extending to both classical and intuitionistic Separation
Logic. We demonstrate the uniformity and modularity of this analysis by
additionally capturing the bunched logics obtained by extending BI and BBI with
modalities and multiplicative connectives corresponding to disjunction,
negation and falsum. This includes the logic of separating modalities (LSM), De
Morgan BI (DMBI), Classical BI (CBI), and the subclassical family of logics
extending Biintuitionistic (B)BI (Bi(B)BI). We additionally obtain as
corollaries soundness and completeness theorems for the specific Kripkestyle
models of these logics as presented in the literature: for DMBI, the
subclassical logics extending BiBI and a new bunched logic, Concurrent Kleene
BI (connecting our work to Concurrent Separation Logic), this is the first time
soundness and completeness theorems have been proved. We thus obtain a
comprehensive semantic account of the multiplicative variants of all standard
propositional connectives in the bunched logic setting. This approach
synthesises a variety of techniques from modal, substructural and categorical
logic and contextualizes the "resource semantics" interpretation underpinning
Separation Logic amongst them.

We present new results on realtime alternating, private alternating, and
quantum alternating automaton models. Firstly, we show that the emptiness
problem for alternating onecounter automata on unary alphabets is undecidable.
Then, we present two equivalent definitions of realtime private alternating
finite automata (PAFAs). We show that the emptiness problem is undecidable for
PAFAs. Furthermore, PAFAs can recognize some nonregular unary languages,
including the unary squares language, which seems to be difficult even for some
classical counter automata with twoway input. Regarding quantum finite
automata (QFAs), we show that the emptiness problem is undecidable both for
universal QFAs on general alphabets, and for alternating QFAs with two
alternations on unary alphabets. On the other hand, the same problem is
decidable for nondeterministic QFAs on general alphabets. We also show that the
unary squares language is recognized by alternating QFAs with two alternations.

Computers may control safetycritical operations in machines having embedded
software. This memoir proposes a regimen to verify such algorithms at
prescribed levels of statistical confidence. The United States Department of
Defense standard for system safety engineering (MILSTD882E) defines
development procedures for safetycritical systems. However, a problem exists:
the Standard fails to distinguish quantitative product assurance technique from
categorical process assurance method for software development. Resulting is
conflict in the technical definition of the term risk. The primary goal here is
to show that a quantitative riskbased product assurance method exists and is
consistent with hardware practice. Discussion appears in two major parts:
theory, which shows the relationship between automata and software; and
application, which covers demonstration and indemnification. Demonstration is a
technique for generating random tests; indemnification converts pass/fail test
results to compound Poisson parameters (severity and intensity). Together,
demonstration and indemnification yield statistical confidence that
safetycritical code meets design intent. Statistical confidence is the
keystone of quantitative product assurance. A secondary goal is resolving the
conflict over the term risk. The first meaning is an accident model known in
mathematics as the compound Poisson stochastic process, and so is called
statistical risk. Various of its versions underlie the theories of safety and
reliability. The second is called developmental risk. It considers software
autonomy, which considers time until manual recovery of control. Once these
meanings are separated, MILSTD882 can properly support either formal
quantitative safety assurance or empirical process robustness, which differ in
impact.

Assigning a satisfactory truly concurrent semantics to Petri nets with
confusion and distributed decisions is a long standing problem, especially if
one wants to resolve decisions by drawing from some probability distribution.
Here we propose a general solution based on a recursive, static decomposition
of (occurrence) nets in loci of decision, called structural branching cells
(scells). Each scell exposes a set of alternatives, called transactions. Our
solution transforms a given Petri net into another net whose transitions are
the transactions of the scells and whose places are those of the original net,
with some auxiliary structure for bookkeeping. The resulting net is
confusionfree, and thus conflicting alternatives can be equipped with
probabilistic choices, while nonintersecting alternatives are purely concurrent
and their probability distributions are independent. The validity of the
construction is witnessed by a tight correspondence with the recursively
stopped configurations of Abbes and Benveniste. Some advantages of our approach
are that: i) scells are defined statically and locally in a compositional way;
ii) our resulting nets faithfully account for concurrency.

Given a graph $F$, let $I(F)$ be the class of graphs containing $F$ as an
induced subgraph. Let $W[F]$ denote the minimum $k$ such that $I(F)$ is
definable in $k$variable firstorder logic. The recognition problem of $I(F)$,
known as Induced Subgraph Isomorphism (for the pattern graph $F$), is solvable
in time $O(n^{W[F]})$. Motivated by this fact, we are interested in determining
or estimating the value of $W[F]$. Using Olariu's characterization of pawfree
graphs, we show that $I(K_3+e)$ is definable by a firstorder sentence of
quantifier depth 3, where $K_3+e$ denotes the paw graph. This provides an
example of a graph $F$ with $W[F]$ strictly less than the number of vertices in
$F$. On the other hand, we prove that $W[F]=4$ for all $F$ on 4 vertices except
the paw graph and its complement. If $F$ is a graph on $t$ vertices, we prove a
general lower bound $W[F]>(1/2o(1))t$, where the function in the littleo
notation approaches 0 as $t$ inreases. This bound holds true even for a related
parameter $W^*[F]\le W[F]$, which is defined as the minimum $k$ such that
$I(F)$ is definable in the infinitary logic $L^k_{\infty\omega}$. We show that
$W^*[F]$ can be strictly less than $W[F]$. Specifically, $W^*[P_4]=3$ for $P_4$
being the path graph on 4 vertices.
Using the lower bound for $W[F]$, we also obtain a succintness result for
existential monadic secondorder logic: A usage of just one monadic quantifier
sometimes reduces the firstorder quantifier depth at a superrecursive rate.

We show that any onecounter automaton with $n$ states, if its language is
nonempty, accepts some word of length at most $O(n^2)$. This closes the gap
between the previously known upper bound of $O(n^3)$ and lower bound of
$\Omega(n^2)$. More generally, we prove a tight upper bound on the length of
shortest paths between arbitrary configurations in onecounter transition
systems (weaker bounds have previously appeared in the literature).

We build a cartesian closed category, called Cho, based on event structures.
It allows an interpretation of higherorder stateful concurrent programs that
is refined and precise: on the one hand it is conservative with respect to
standard HylandOng games when interpreting purely functional programs as
innocent strategies, while on the other hand it is much more expressive. The
interpretation of programs constructs compositionally a representation of their
execution that exhibits causal dependencies and remembers the points of
nondeterministic branching.The construction is in two stages. First, we build
a compact closed category Tcg. It is a variant of Rideau and Winskel's category
CG, with the difference that games and strategies in Tcg are equipped with
symmetry to express that certain events are essentially the same. This is
analogous to the underlying category of AJM games enriching simple games with
an equivalence relations on plays. Building on this category, we construct the
cartesian closed category Cho as having as objects the standard arenas of
HylandOng games, with strategies, represented by certain events structures,
playing on games with symmetry obtained as expanded forms of these arenas.To
illustrate and give an operational light on these constructions, we interpret
(a close variant of) Idealized Parallel Algol in Cho.

A C*algebra is determined to a great extent by the partial order of its
commutative C*algebras. We study ordertheoretic properties of this dcpo. Many
properties coincide: the dcpo is, equivalently, algebraic, continuous,
meetcontinuous, atomistic, quasialgebraic, or quasicontinuous, if and only
if the C*algebra is scattered. For C*algebras with enough projections, these
properties are equivalent to finitedimensionality. Approximately
finitedimensional elements of the dcpo correspond to Boolean subalgebras of
the projections of the C*algebra, which determine the projections up to
isomorphism. Scattered C*algebras are finitedimensional if and only if their
dcpo is Lawsonscattered. General C*algebras are finitedimensional if and
only if their dcpo is orderscattered.

Recent developments in formal verification have identified approximate
liftings (also known as approximate couplings) as a clean, compositional
abstraction for proving differential privacy. This construction can be defined
in two styles. Earlier definitions require the existence of one or more witness
distributions, while a recent definition by Sato uses universal quantification
over all sets of samples. These notions have each have their own strengths: the
universal version is more general than the existential ones, while existential
liftings are known to satisfy more precise composition principles.
We propose a novel, existential version of approximate lifting, called
$\star$lifting, and show that it is equivalent to Sato's construction for
discrete probability measures. Our work unifies all known notions of
approximate lifting, yielding cleaner properties, more general constructions,
and more precise composition theorems for both styles of lifting, enabling
richer proofs of differential privacy. We also clarify the relation between
existing definitions of approximate lifting, and consider more general
approximate liftings based on $f$divergences.

We study rewritability of monadic disjunctive Datalog programs, (the
complements of) MMSNP sentences, and ontologymediated queries (OMQs) based on
expressive description logics of the ALC family and on conjunctive queries. We
show that rewritability into FO and into monadic Datalog (MDLog) are decidable,
and that rewritability into Datalog is decidable when the original query
satisfies a certain condition related to equality. We establish
2NExpTimecompleteness for all studied problems except rewritability into MDLog
for which there remains a gap between 2NExpTime and 3ExpTime. We also analyze
the shape of rewritings, which in the MMSNP case correspond to obstructions,
and give a new construction of canonical Datalog programs that is more
elementary than existing ones and also applies to formulas with free variables.

The present paper gives a generalization of cartesian closed categories,
called cartesian closed categories with dependence, whose strict version
induces categories with families that support 1, Sigma and Pitypes in the
strict sense. Consequently, we have obtained a new semantics of dependent type
theories that is both categorical and truetosyntax.

We introduce the notion of feedback computable functions from $2^\omega$ to
$2^\omega$, extending feedback Turing computation in analogy with the standard
notion of computability for functions from $2^\omega$ to $2^\omega$. We then
show that the feedback computable functions are precisely the effectively Borel
functions. With this as motivation we define the notion of a feedback
computable function on a structure, independent of any coding of the structure
as a real. We show that this notion is absolute, and as an example characterize
those functions that are computable from a Gandy ordinal with some finite
subset distinguished.

We carry out a proof theoretic analysis of the wellfoundedness of recursive
path orders in an abstract setting. We outline a very general termination
principle and extract from its wellfoundedness proof subrecursive bounds on the
size of derivation trees which can be defined in G\"{o}del's system T plus bar
recursion. We then carry out a complexity analysis of these terms, and
demonstrate how this can be applied to bound the derivational complexity of
term rewrite systems.

Unambiguous automata are nondeterministic automata in which every word has at
most one accepting run. In this paper we give a polynomialtime algorithm for
model checking discretetime Markov chains against $\omega$regular
specifications represented as unambiguous automata. We furthermore show that
the complexity of this model checking problem lies in NC: the subclass of P
comprising those problems solvable in polylogarithmic parallel time. These
complexity bounds match the known bounds for model checking Markov chains
against specifications given as deterministic automata, notwithstanding the
fact that unambiguous automata can be exponentially more succinct than
deterministic automata. We report on an implementation of our procedure,
including an experiment in which the implementation is used to model check LTL
formulas on Markov chains.