From db91773c8140a69dc42a954cf93505a1496a217c Mon Sep 17 00:00:00 2001
From: Luigi Santocanale <luigi.santocanale@lif.univ-mrs.fr>
Date: Thu, 4 Nov 2021 19:04:16 +0100
Subject: [PATCH] 	modified:   index.html

---
 index.html | 34 ++++++++++++++++++++++++++++++++++
 1 file changed, 34 insertions(+)

diff --git a/index.html b/index.html
index 7907d0f..ba4a283 100644
--- a/index.html
+++ b/index.html
@@ -324,6 +324,7 @@
 <a href="javascript:toggleDiv('T1')">Free Modal Riesz Spaces are Archimedean: a Syntactic Proof</a>
 <div style="display:none", id="T1"><br /><br />We prove, using syntactical proof–theoretic methods, that free modal Riesz spaces are Archimedean. Modal Riesz spaces are Riesz spaces (real vector lattices) endowed with a positive linear 1–decreasing operator, and have found application in the development of probabilistic temporal logics in the field of formal verification. All our results have been formalised using the Coq proof assistant.</div>
 </td>
+<td><a href="pdfs/Tue09h00/Lucas.pdf">Slides</a></td>
 </tr>
 
 
@@ -336,6 +337,7 @@
 <a href="javascript:toggleDiv('T2')">Some modal and temporal translations of generalized basic logic</a>
 <div style="display:none", id="T2"><br /><br />We introduce a family of modal expansions of Łukasiewicz logic that are designed to accommodate modal translations of generalized basic logic (as formulated with exchange, weakening, and falsum). We further exhibit algebraic semantics for each logic in this family, in particular showing that all of them are algebraizable in the sense of Blok and Pigozzi. Using this algebraization result, we establish that each of the introduced modal Łukasiewicz logics has a local deduction detachment theorem. By applying Jipsen and Montagna's poset product construction, we give two translations of generalized basic logic with exchange, weakening, and falsum in the style of the celebrated Gödel-McKinsey-Tarski translation. The first of these interprets generalized basic logic in a modal Łukasiewicz logic in the spirit of classical S4, whereas the second interprets generalized basic logic in a temporal variant of the latter.</div>
 </td>
+<td><a href="pdfs/Tue09h00/Fussner.pdf">Slides</a></td>
 </tr>
 
 
@@ -348,6 +350,8 @@
 <a href="javascript:toggleDiv('T3')">Algorithmic correspondence for relevance logics, bunched implication logics, and relation algebras via an implementation of the algorithm PEARL</a>
 <div style="display:none", id="T3"><br /><br />The theory and methods of algorithmic correspondence theory for modal logics, developed over the past 20 years, have recently been extended to the language RL of relevance logics with respect to their standard Routley-Meyer relational semantics. As a result, the non-deterministic algorithmic procedure PEARL (acronym for 'Propositional variables Elimination Algorithm for Relevance Logic') has been developed for computing first-order equivalents of formulae of the language RL in terms of that semantics. PEARL is an adaptation of the previously developed algorithmic procedures SQEMA (for normal modal logics) and ALBA (for distributive and non-distributive modal logics). It succeeds on all inductive formulae in the language RL, in particular on all previously studied classes of Sahlqvist formulae for relevance logic. In the present work, we re-interpret the algorithm PEARL from an algebraic perspective with its rewrite rules seen as manipulating quasi-inequalities interpreted over Urquhart's relevant algebras. This enables us to complete the part of the Sahlqvist theorem still outstanding from the previous work, namely the fact that all inductive RL formulas are canonical, i.e., are preserved under canonical extensions of relevant algebras. Via the discrete duality between perfect relevant algebras and Routley-Meyer frames, this establishes the fact that all inductive RL formulas axiomatise logics which are complete with respect to first-order definable classes of Routley-Meyer frames. This generalizes the "canonicity via correspondence" result in [Urquhart, 1996] for (what we can now recognise as) a certain special subclass of Sahlqvist formulas in the "groupoid" sublanguage of RL where fusion is the only connective. By extending RL with a unary connective for converse and adding the necessary axioms, our results can also be applied to bunched implication algebras and relation algebras. We then present an optimised and deterministic version of PEARL, which we have recently implemented in Python and applied to verify the first-order equivalents of a number of important axioms for relevance logics known from the literature, as well as on several new types of formulae. In the paper, we report on the implementation and on some testing results.</div>
 </td>
+<td><a href="pdfs/Tue09h00/Jipsen.pdf">Slides</a></td>
+
 </tr>
 
 
@@ -367,6 +371,7 @@
 <a href="javascript:toggleDiv('T4')">Computing Aggregated Knowledge as the Greatest Lower Bound of Knowledge</a>
 <div style="display:none", id="T4"><br /><br />In economics and multi-agent systems, <i>aggregated (or distributed) knowledge</i> of a group is the knowledge of someone who knows exactly what every member of the group knows. This notion can be used to analyse the implications of the knowledge of a community if they were to combine their knowledge. In this paper we use fundamental tools from the theory of distributive lattice to characterize and compute aggregate knowledge.We prove that for distributive lattices of size $n$, (1) the meet of join-endomorphisms can be computed in time $O(n)$. Previous upper bound was $O(n^2)$. We show that (2) aggregated knowledge of given group can be viewed as the meet of the knowledge of each member of the group. We also show that for state sets of size $n$, (3) aggregated knowledge can be computed in time $O(n^2)$ in the general case and (4) for $S5$ knowledge (or <i>Aumman structures</i>), it can be computed in time $O(n\alpha(n))$ where $\alpha(n)$ is the inverse of the Ackermann function.</div>
 </td>
+<td><a href="pdfs/Tue11h00/Ramirez.pdf">Slides</a></td>
 </tr>
 
 
@@ -379,6 +384,9 @@
 <a href="javascript:toggleDiv('T5')">lr-Multisemigroups, Modal Quantales and the Origin of Locality</a>
 <div style="display:none", id="T5"><br /><br />We introduce lr-multisemigroups as duals of modal quantales and study correspondences between equations in these multisemigroups and the domain and codomain axioms of modal quantales. Our results yield construction principles for modal powerset quantales that cover a wide range of models and applications.</div>
 </td>
+
+<td><a href="pdfs/Tue11h00/Struth.pdf">Slides</a></td>
+
 </tr>
 
 
@@ -391,6 +399,7 @@
 <a href="javascript:toggleDiv('T6')">Polyadic spaces and profinite monoids</a>
 <div style="display:none", id="T6"><br /><br />Hyperdoctrines are an algebraization of first-order logic introduced by Lawvere. Joyal proposed to apply pointwise Stone duality to get what he called a polyadic space. He also proposed the idea of Stirling kernels of a polyadic space that we generalize here in order to adapt the notion of polyadic space to certain special classes of first-order theories. We will see how these ideas can be applied to establish a correspondence between equidivisible profinite semigroups with open multiplication and some first-order theories with a linear order symbol.</div>
 </td>
+<td><a href="pdfs/Tue11h00/Marques.pdf">Slides</a></td>
 </tr>
 
 
@@ -444,6 +453,8 @@ QCSP to be PSpace-hard.
 In the talk I will discuss the above and some other results.
 </div>
 </td>
+<td><a href="pdfs/Tue14h00/Zhuk.pdf">Slides</a></td>
+
 </tr>
 
 
@@ -456,6 +467,7 @@ In the talk I will discuss the above and some other results.
 <a href="javascript:toggleDiv('T8')">Unary-determined distributive l-magmas and bunched implication algebras</a>
 <div style="display:none", id="T8"><br /><br />A distributive lattice-ordered magma ($d\ell$-magma) $(A,\wedge,\vee,\cdot)$ is a distributive lattice with a binary operation $\cdot$ that preserves joins in both arguments, and when $\cdot$ is associative then $(A,\vee,\cdot)$ is an idempotent semiring. A $d\ell$-magma with a top $\top$ is <i>unary-determined</i> if $x\cdot y=(x\top\wedge y)\vee(x\wedge \top y)$. These algebras are term-equivalent to a subvariety of distributive lattices with $\top$ and two join-preserving unary operations $p,q$. We obtain simple conditions on $p,q$ such that $x\cdot y=(px\wedge y)\vee(x\wedge qy)$ is associative, commutative, idempotent and/or has an identity element. This generalizes previous results on the structure of doubly idempotent semirings and, in the case when the distributive lattice is a Heyting algebra, it provides structural insight into unary-determined algebraic models of bunched implication logic. We also provide Kripke semantics for the algebras under consideration, which leads to more efficient algorithms for constructing finite models.</div>
 </td>
+<td><a href="pdfs/Tue14h00/Sugimoto.pdf">Slides</a></td>
 </tr>
 
 
@@ -474,6 +486,8 @@ In the talk I will discuss the above and some other results.
 <a href="javascript:toggleDiv('T9')">Many-valued modal logic over a semi-primal algebra (short talk)</a>
 <div style="display:none", id="T9"><br /><br />Since semi-primal algebras behave similarly to the two-element Boolean algebra, it makes sense to consider many-valued logic over a semi-primal algebra of truth values. Our interest lies in modal extensions of such logics. Through their respective dual categories we explore the relationship between the variety HSP(L) generated by a semi-primal algebra L and the variety BA of Boolean algebras. As an example, we utilize this relationship to prove a many-valued analogue of the Goldblatt-Thomason Theorem. Furthermore, we discuss the underlying coalgebraic picture and discuss how one may lift results from the classical case to the many-valued case.</div>
 </td>
+<td><a href="pdfs/Tue16h00/Poiger.pdf">Slides</a></td>
+
 </tr>
 
 
@@ -486,6 +500,7 @@ In the talk I will discuss the above and some other results.
 <a href="javascript:toggleDiv('T10')">Amalgamation property for varieties of BL-algebras generated by one chain with finitely many components</a>
 <div style="display:none", id="T10"><br /><br />BL-algebras are the algebraic semantics for Hajek's Basic Logic BL, the logic of all continuous t-norms and their residua. In this paper we study the amalgamation property for the varieties of BL-algebras generated by one BL-chain with finitely many components.</div>
 </td>
+<td><a href="pdfs/Tue16h00/Bianchi.pdf">Slides</a></td>
 </tr>
 
 
@@ -511,6 +526,7 @@ by the antiortholattices with the Strong De Morgan property and the ordinal sum
 The form of this lattice isomorphism proves that the variety PKA is generated by the class of the bounded involution lattice reducts of the members of SAOL, thus also by the quasivariety of paraortho- modular pseudo–Kleene algebras and by the class of the bounded involution lattice reducts of the members of PBZL∗, which also shows that neither of these classes is a variety.
 We obtain an infinite ascending chain of varieties of distributive PBZ∗–lattices, which, along with the well–known infinite ascending chain of varieties of modular ortholattices and its image through the lattice isomorphism mentioned above, give us an infinity of pairwise disjoint infinite ascending chains of varieties of PBZ∗–lattices.</div>
 </td>
+<td><a href="pdfs/Tue16h00/Muresan.pdf">Slides</a></td>
 </tr>
 
 
@@ -523,6 +539,7 @@ We obtain an infinite ascending chain of varieties of distributive PBZ∗–latt
 <a href="javascript:toggleDiv('T12')">On the Representation Number of Bipartite Graphs (short talk)</a>
 <div style="display:none", id="T12"><br /><br />A word-representable graph is a simple graph G which can be represented by a word w over the vertices of G such that any two vertices are adjacent in G if and only if they alternate in w. It is known that the class of comparability graphs – the graphs which admit a transi- tive orientation – is precisely the class of graphs that can be represented by a concatenation of permutations of vertices. The class of bipartite graphs is a subclass of comparability graphs. While it is an open prob- lem to determine the representation number of comparability graphs, it was conjectured that the representation number of bipartite graphs on n vertices is at most n/4. In this paper, we propose a polynomial time relabeling algorithm to produce a word representing a given bipartite graph which is a concatenation of permutations of the graph’s vertices. Thus we obtain an upper bound for the representation number of bipar- tite graphs, which in turn gives us an upper bound for the dimension of the posets corresponding to bipartite graphs.</div>
 </td>
+<td><a href="pdfs/Tue16h00/Mozhui.pdf">Slides</a></td>
 </tr>
 
 
@@ -544,6 +561,7 @@ We obtain an infinite ascending chain of varieties of distributive PBZ∗–latt
 <a href="javascript:toggleDiv('T13')">Effect Algebras, Girard Quantales and Complementation in Separation Logic</a>
 <div style="display:none", id="T13"><br /><br />We study convolution and residual operations within convolution quantales of maps from partial abelian semigroups and effect algebras into value quantales, thus generalising separating conjunction and implication of separation logic to quantitative settings. We show that effect algebras lift to Girard convolution quantales, but not the standard partial abelian monoids used in separation logic. This shows that the standard assertion quantales of separation logic do not admit a linear negation relating convolution and its right adjoint. We consider alternative dualities for these operations on convolution quantales using boolean negations, some old, some new, relate them with properties of the underlying partial abelian semigroups and outline potential uses.</div>
 </td>
+<td><a href="pdfs/Wed09h00/Bannister.pdf">Slides</a></td>
 </tr>
 
 
@@ -556,6 +574,7 @@ We obtain an infinite ascending chain of varieties of distributive PBZ∗–latt
 <a href="javascript:toggleDiv('T14')">Skew metrics valued in Sugihara semigroups</a>
 <div style="display:none", id="T14"><br /><br />We consider skew metrics (equivalently, transitive relations that are tournaments, linear orderings) valued in Sugihara semigroups on autodual chains. We prove that, for odd chains and chains without a unit, skew metrics classify certain tree-like structures that we call perfect augmented plane towers. When the chain is finite and has cardinality $2K+1$, skew metrics on a set $X$ give rise to plane rooted trees of height $K$ whose frontier is a linear preorder of $X$.Any linear ordering on $X$ gives rise to an ordering on the set of its skew metrics valued on an arbitrary involutive residuated lattice $Q$. If $Q$ satisfies the mix rule, then this poset is most often a lattice. We study this lattice for $X = \{1,\ldots ,n\}$ and $Q$ the Sugihara monoid on the chain of cardinality $2K+1$. We give a combinatorial model of this lattice by describing its covers as moves on a appropriate space of words coding perfect augmented plane trees. Using the combinatorial model, we develop enumerative considerations on this lattice.</div>
 </td>
+<td><a href="pdfs/Wed09h00/Santocanale.pdf">Slides</a></td>
 </tr>
 
 
@@ -568,6 +587,7 @@ We obtain an infinite ascending chain of varieties of distributive PBZ∗–latt
 <a href="javascript:toggleDiv('T15')">Time Warps, from Algebra to Algorithms</a>
 <div style="display:none", id="T15"><br /><br />Graded modalities have been proposed in recent work on programming languages as a general framework for refining type systems with intensional properties. In particular, continuous endomaps of the discrete time scale, or time warps, can be used to quantify the growth of information in the course of program execution. Time warps form a complete residuated lattice, with the residuals playing an important role in potential programming applications. In this paper, we study the algebraic structure of time warps, and prove that their equational theory is decidable, a necessary condition for their use in real-world compilers. We also describe how our universal-algebraic proof technique lends itself to a constraint-based implementation, establishing a new link between universal algebra and verification technology.</div>
 </td>
+<td><a href="pdfs/Wed09h00/Santschi.pdf">Slides</a></td>
 </tr>
 
 
@@ -586,6 +606,7 @@ We obtain an infinite ascending chain of varieties of distributive PBZ∗–latt
 <a href="javascript:toggleDiv('T16')">Isolated Sublattices and their Application to Counting Closure Operators</a>
 <div style="display:none", id="T16"><br /><br />This paper is dedicated to the investigation of the interplay between isolated sublattices and closure operators.Isolated sublattices are a special kind of sublattices which can serve to diminuish the number of elements of a lattice by means of a quotient lattice.At the same time, there are simple formulae for the relationship between the number of closure operators in the original lattice and its quotient.This connection can be used to derive an algorithm for counting closure operators, provided the lattice contains suitable isolated sublattices.</div>
 </td>
+<td><a href="pdfs/Wed11h00/Glueck.pdf">Slides</a></td>
 </tr>
 
 
@@ -598,6 +619,7 @@ We obtain an infinite ascending chain of varieties of distributive PBZ∗–latt
 <a href="javascript:toggleDiv('T17')">A Variety Theorem for Relational Universal Algebra</a>
 <div style="display:none", id="T17"><br /><br />We consider an analogue of universal algebra in which generating symbols are interpreted as relations. We prove a variety theorem for these relational algebraic theories, in which we find that their categories of models are precisely the definable categories. The syntax of our relational algebraic theories is string-diagrammatic, and can be seen as an extension of the usual term syntax for algebraic theories.</div>
 </td>
+<td><a href="pdfs/Wed11h00/Nester.pdf">Slides</a></td>
 </tr>
 
 
@@ -610,6 +632,7 @@ We obtain an infinite ascending chain of varieties of distributive PBZ∗–latt
 <a href="javascript:toggleDiv('T18')">Abstract Strategies and Coherence</a>
 <div style="display:none", id="T18"><br /><br />Normalisation strategies give a categorical interpretation of the notion of contracting homotopies via confluent and terminating rewriting. This approach relates standardisation to coherence results in the context of higher dimensional rewriting systems. On the other hand, globular 2-Kleene algebras provide a formal setting for reasoning about coherence proofs in abstract rewriting systems. In this work, we formalise the notion of normalisation strategy in this setting. In such structures, normalisation strategies allow us to prove a formal coherence theorem via convergent abstract rewriting.</div>
 </td>
+<td><a href="pdfs/Wed11h00/Calk.pdf">Slides</a></td>
 </tr>
 
 
@@ -638,6 +661,7 @@ will show how the technique allows one to distribute SAT-based
 bug-finding as well as symbolic execution over
 complex data types.</div>
 </td>
+<td><a href="pdfs/Wed14h30/Frias.pdf">Slides</a></td>
 </tr>
 
 
@@ -656,6 +680,7 @@ complex data types.</div>
 <a href="javascript:toggleDiv('T20')">Change of Base using Arrow Categories</a>
 <div style="display:none", id="T20"><br /><br />Arrow categories establish a suitable framework to reason about L-fuzzy relation abstractly. For each arrow category we can identify the Heyting algebra L that is used as the lattice of membership or truth values by the relations of the category. Therefore, arrow categories model the fixed-base approach to L-fuzziness, i.e., all relations of the given arrow category use the same membership values. In this paper we are interested in the process of changing the base, i.e., an operation that allows to switch from an L1-fuzzy relation to an L2-fuzzy relation by replacing all membership values from L1 by values from L2 . We will define and investigate this change of base between two abstract arrow categories for which component-wise reasoning cannot be performed.</div>
 </td>
+<td><a href="pdfs/Wed16h00/Winter-ChangeOfBase.pdf">Slides</a></td>
 </tr>
 
 
@@ -668,6 +693,7 @@ complex data types.</div>
 <a href="javascript:toggleDiv('T21')">L-fuzzy Concept Analysis using Arrow Categories (short talk)</a>
 <div style="display:none", id="T21"><br /><br />The purpose of this paper is to investigate topics in fuzzy concept analysis using the theory of arrow categories. Our approach deals with the origi- nal, fuzzy data using fuzzy subsets in order to obtain a notion of fuzzy concepts, fuzzy concept lattices, and fuzzy association rules. Our approach is general in the sense that we only require a complete Heyting algebra as the lattice of truth values instead of the unit interval r0, 1s or a substructure thereof. In addition, our approach differs from most approaches in the literature, which usually first apply some kind of defuzzyfication, e.g., α-cuts, and then apply concept analysis in the classical (crisp) sense.</div>
 </td>
+<td><a href="pdfs/Wed16h00/Winter-FCS.pdf">Slides</a></td>
 </tr>
 
 
@@ -680,6 +706,7 @@ complex data types.</div>
 <a href="javascript:toggleDiv('T22')">Accretive Computation of Global Transformations</a>
 <div style="display:none", id="T22"><br /><br />Global transformations form a categorical framework adapting graph transformations to describe fully synchronous rule systems on a given data structure. In this work we focus on data structures that can be captured as presheaves (like sets, graphs or Petri nets) and study the computational aspects of such synchronous rule systems. To obtain an online algorithm, a complete study of the sub-steps within each synchronous step is done at the semantic level. This leads to the definition of accretive rule systems and a local criterion to characterize these systems. Finally an online computation algorithm for theses systems is given.</div>
 </td>
+<td><a href="pdfs/Wed16h00/Fernandez.pdf">Slides</a></td>
 </tr>
 
 
@@ -704,6 +731,7 @@ complex data types.</div>
 <a href="javascript:toggleDiv('T24')">Generalizing Girard quantale in a symmetric closed monoidal category (short talk)</a>
 <div style="display:none", id="T24"><br /><br />The category of complete lattices and join-preserving maps is known to be star-autonomous and the semigroup of this category are called quan- tales. A Frobenius quantale is usually defined as a quantale with a du- alizing element. If this element is also cyclic, the quantale is called a Girard quantale and it can interpret the non-commutative linear logic. Two properties have motivated this work. First, the canonical quantale of endomorphism of a complete lattice is a Girard quantale if and only if this lattice is completely distributive. Secondly, completely distributive lattices have a categorical characterization: they are exactly the nuclear objects – i.e the mix arrow is an isomorphism – of the category of sup lattices. The aim of this work was to find out the kind of semigroup (we simply called them Girard semigroup) that generalize Girard quantale. With the right definition in hand we wanted to verify if the following con- jecture is satisfied: given a symetric closed monoidal category, the internal hom of an object with itself is a Girard semigroup if and only if this object is a nuclear object of the category – that is if the generalization of the above property is still true. We used a - slightly - more general definition of Frobenius and Girard quantales which led to a suitable definition of Frobenius and Girard semigroups in any symetric closed category. In this work we found several properties of these new structures and we proved that if an object is nuclear then the internal hom of this object with it- self has a structure of Girard semigroup. The converse implication of the conjecture is still to be proved.</div>
 </td>
+<td><a href="pdfs/Wed16h00/Delacroix.pdf">Slides</a></td>
 </tr>
 
 
@@ -724,6 +752,7 @@ complex data types.</div>
 <a href="javascript:toggleDiv('T25')">On Algebra of Program Correctness and Incorrectness</a>
 <div style="display:none", id="T25"><br /><br />Variations on the notion of Kleene algebra have been used to provide foundations of reasoning about programs, for instance by showing how Hoare Logic (HL) can be represented in algebra. This line of work has focussed on program correctness,i.e., proving the absence of bugs. Recently, Incorrectness Logic (IL) has been advanced as a reasoning formalism for the dual problem: proving the presence of bugs. IL is intended to underpin the use of logic in program testing and static bug finding. In this paper we describe an extension of Kleene algebra, an algebra with backwards diamond operators and countable joins for tests, which embeds IL, and which also is complete for reasoning about the image of the embedding. In addition to embedding IL, the algebra retains the ability to embed HL, and to make connections between IL and HL specifications: In this sense, it unifies correctness and incorrectness reasoning in one formalism.</div>
 </td>
+<td><a href="pdfs/Thu09h00/Moeller.pdf">Slides</a></td>
 </tr>
 
 
@@ -736,6 +765,7 @@ complex data types.</div>
 <a href="javascript:toggleDiv('T26')">Second-Order Properties of Undirected Graphs</a>
 <div style="display:none", id="T26"><br /><br />We study second-order formalisations of graph properties expressed as first-order formulas in relation algebras extended with a Kleene star. The formulas quantify over relations while still avoiding quantification over elements of the base set. We formalise the property of undirected graphs being acyclic this way. This involves a study of various kinds of orientation of graphs. We also verify basic algorithms to constructively prove several second-order properties.</div>
 </td>
+<td><a href="pdfs/Thu09h00/Guttmann.pdf">Slides</a></td>
 </tr>
 
 
@@ -748,6 +778,7 @@ complex data types.</div>
 <a href="javascript:toggleDiv('T27')">Relation-algebraic Verification of Borůvka's Minimum Spanning Tree Algorithm</a>
 <div style="display:none", id="T27"><br /><br />Previous work introduced a relation-algebraic framework for reasoning about weighted-graph algorithms. We use this framework to prove partial correctness of Borůvka's minimum spanning tree algorithm. This is the first formal proof of correctness for this algorithm. We also discuss new abstractions that make it easier to reason about weighted graphs.</div>
 </td>
+<td><a href="pdfs/Thu09h00/OBrien.pdf">Slides</a></td>
 </tr>
 
 
@@ -766,6 +797,7 @@ complex data types.</div>
 <a href="javascript:toggleDiv('T28')">Experimental Investigation of Sufficient Criteria for Relations to Have Kernels</a>
 <div style="display:none", id="T28"><br /><br />We investigate four well-known criteria for the existence of kernels in directed graphs/relations which efficiently can be tested, namely to be irreflexive and symmetric, to be progressively finite, to be bipartite, and to satisfy Richardson's criterion. The numerical data, obtained by the evaluation of relation-algebraic problem specifications by means of RelView, show that even the most general of them is very far away from a characterisation of the class of directed graphs having kernels.</div>
 </td>
+<td><a href="pdfs/Thu11h00/Berghammer_1.pdf">Slides</a></td>
 </tr>
 
 
@@ -778,6 +810,7 @@ complex data types.</div>
 <a href="javascript:toggleDiv('T29')">Relational Computation of Sets of Relations</a>
 <div style="display:none", id="T29"><br /><br />We present a technique for the relational computation of sets RR of relations. It is based on a specification of a relation R to belong to RR by means of an inclusion $s \subseteq t$, where s and t are relation-algebraic expressions constructed from a vector model of R in a specific way. To get the inclusion, we apply properties of a mapping that transforms relations into their vectors models and, if necessary, point-wise reasoning. The desired computation of RR via a relation-algebraic expression r is then immediately obtained from the inclusion using a result published in the proceedings of MPC 2015. Compared with a direct development of r from a logical specification of R to belong to RR, the proposed technique is much more simple. We demonstrate its use by some classes of specific relations and also show some applications.</div>
 </td>
+<td><a href="pdfs/Thu11h00/Berghammer_2.pdf">Slides</a></td>
 </tr>
 
 
@@ -790,6 +823,7 @@ complex data types.</div>
 <a href="javascript:toggleDiv('T30')">Automated Reasoning for Probabilistic Sequential Programs with Theorem Proving</a>
 <div style="display:none", id="T30"><br /><br />Semantics for nondeterministic probabilistic sequential programs is well studied in the past decades. In a variety of semantic models, how nondeterministic choice interacts with probabilistic choice is the most significant difference. In He, Morgan, and McIver’s relational model, probabilistic choice refines nondeterministic choice. This model is general because of its predicative-style semantics in Hoare and He’s Unifying Theories of Programming, and suitable for automated reasoning because of its algebraic feature. Previously, we gave probabilistic semantics to the RoboChart notation based on this model, and also formalised its proof, and revealed interesting details. In this paper, we present our mechanisation of the proof in Isabelle/UTP, an Isabelle/HOL based proof framework for UTP, enabling automated reasoning for probabilistic sequential programs including a subset of the RoboChart language. With mechanisation, we even reveal more interesting questions, hidden in the original model. We demonstrate several examples, including an example to illustrate the interaction between nondeterministic choice and probabilistic choice, and a RoboChart model for randomisation based on binary probabilistic choice.</div>
 </td>
+<td><a href="pdfs/Thu11h00/Ye.pdf">Slides</a></td>
 </tr>
 
 
-- 
GitLab