*Abstract:* In this talk I will discuss the interplay between
two important topics in programming language research: dependent types
and computational effects; by defining a small dependently-typed
language, combining the features of Martin-Löf type theory and
computational languages such as Call-By-Push-Value and the Enriched
Effect Calculus. Our language has both value types and terms and
computation types and terms, with the value and computation types only
allowed to depend on values. A novel aspect of our language is the use
of computational sigma-types to account for type-dependency in the
sequential composition of computations.

The design of our language is inspired by a class of categorical models we call fibred adjunction models. These naturally combine i) comprehension categories arising from the semantics of dependent types; and ii) adjunctions arising from the semantics of computational effects. We also discuss a variety of examples, some arising from EM-algebras of monads, some from other decompositions of monads into adjunctions and some from considering general recursion as a computational effect.

Finally, we also comment on some ongoing work on understanding parametrized adjunctions and parametrized computational effects in this fibred setting. In particular, we show how the clear distinction between values and computations sheds new light on how to model parametrized computational effects where the result parameters need to depend on result values, for example, to model the possible failure of opening a file.

This is joint work with Neil Ghani and Gordon Plotkin.

Slides from the talk [pdf]

*Abstract:* Illumination enhancement has been a challenging
topic in the field of image/video processing, not only because it
plays an important role in many image processing applications, but
also because it directly effects on the scene. This talk is divided
into two parts. Firstly we will talk about some state-of-the-art
techniques, which are being used in illumination enhancement of 8-bit
images, such as singular value decomposition based illumination
enhancement, wavelet transform based illumination enhancement, and
Gaussian distribution mapping based contrast stretching. Then we will
introduce the new era of digital imaging, which is known as high
dynamic range (HDR) imaging. In the latter part we will talk about
the challenges present in HDR imaging as well as the importance of
illumination enhancement on solving flickers problems in this
field.

Slides from the talk [pptx]

*Abstract:* This talk will outline a method for diagnosing
behavioral differences between pairs of business process models. Given
two process models, the method determines if they are behaviorally
equivalent, and if not, it describes their differences in terms of
behavioral relations captured in one model but not in the other. The
method is based on a translation from process models to event
structures. A naive version of this translation suffers from two
limitations. First, this translation is not applicable to process
models with cycles. Second, it produces redundant difference
diagnostic statements because an event structure may contain
unnecessary event duplication. To tackle the first limitation, we
propose a notion of unfolding that captures all possible causes of
each task, where tasks that can occur more than once in a run are
distinguished from those that cannot. From this unfolding, an event
structure is derived, thus enabling the diagnosis of behavioral
differences in terms of repetition and behavioral relations that hold
in one model but not in the other. For the second limitation, we put
forward a technique to reduce event duplication in an event structure
while preserving canonicity, by applying a set of behavior-preserving
event folding rules. The proposed method has been implemented as a
prototype that takes pairs of process models in the Business Process
Model and Notation (BPMN) and produces difference diagnostics both in
the form of statements in natural language and graphically overlaid on
the process models.

Slides from the talk [pdf]

*Abstract:* Cellular automata (briefly, CA) are parallel
synchronous systems on regular grids where the next state of a point
depends on the current state of a finite neighborhood. The grid is
determined by a finitely generated group and can be visualized as the
Cayley graph of the group according to a suitable set of
generators. In addition to being a useful tool for simulations, CA
also raise important and interesting questions, such as how properties
of the global transition function (obtained by synchronous application
of the local update rule at each point) are linked to each other, and
to properties of the underlying group.

We call a cellular automaton post-surjective if, however given a
configuration *X* and a preimage *Y* to *X*, every
configuration asymptotic (i.e., equal outside a finite set)
to *X* has a preimage asymptotic to *Y*. The well known dual
concept is pre-injectivity: a cellular automaton is pre-injective if
distinct asymptotic configurations have distinct images. We prove
that, under an assumption on the underlying group for which no
counterexamples are known, cellular automata which are both
pre-injective and post-surjective admit a reverse CA. In particular,
because of the famous Garden of Eden theorem, *d*-dimensional
post-surjective CA are reversible.

This is joint work with Jarkko Kari and Siamak Taati, presented at AUTOMATA 2015.

Slides from the talk [pdf]

*Abstract:* This paper deals with computational aspects of
attack trees, more precisely, evaluating the expected adversarial
utility in the failurefree game, where the adversary is allowed to
re-run failed atomic attacks an unlimited number of times. It has been
shown by Buldas and Lenin that exact evaluation of this utility is an
NP-complete problem, so a computationally feasible approximation is
needed. In this paper we consider a genetic approach for this
challenge. Since genetic algorithms depend on a number of non-trivial
parameters, we now have a multi-objective optimization problem and we
consider several heuristic criteria to solve it.

This is joint work with Aleksandr Lenin and Jan Willemson.

Slides from the talk [pdf]

*Abstract:* Process mining is a family of methods to analyze
event logs produced during the execution of business processes in
order to extract insights regarding their performance and conformance
with respect to normative or expected behavior. The landscape of
process mining methods and use cases has expanded considerably in the
past decade. However, the field has evolved in a rather ad hoc manner
without a unifying foundational theory that would allow algorithms and
theoretical results developed for one process mining problem to be
reused when addressing other related problems. In this talk we will
advocate a foundational approach to process mining based on a
well-known model of concurrency, namely event structures. We outline
how event structures can serve as a unified representation of behavior
captured in process models and behavior captured in event logs. We
then sketch how process mining operations, specifically automated
process discovery, conformance checking and deviance mining, can be
recast as operations on event structures.

*Abstract:* The problem of business process conformance
checking is defined as follows: Given an event log recording the
actual execution of a business process, and given a process model
capturing its expected or normative execution, describe the
differences between the behavior captured in the event log and that
captured in the process model.

This talk will outline a novel business process conformance checking method based on event structures. The talk will show that the problem of conformance checking can be approached by folding the event log into an event structure, unfolding the process model into another event structure, and comparing the two event structures via an error-correcting synchronized product.

*Abstract:* The use of cellular phones has increased in recent
years, as has the amount of data collected about the devices and their
users. This collected information can be used to understand human
mobility as well as human behavior. However, the fact that cellular
data is sparse and spatio-temporal rises up many challenges regarding
the temporal and geographical representation of human mobility or
movement. From this perspective, analyzing and investigating the data
helps significantly when constructing models to represent the real
movement of people and also predict their mobility behavior.

Slides from the talk [pdf]

*Abstract*: Business process matching is the activity of
checking whether a given business process can interoperate with
another one in a correct manner. In case the check fails, it is
desirable to obtain information about how the first process can be
corrected with as few modifications as possible to achieve
interoperability. In case the two business processes belong to two
separate enterprises that want to build a virtual enterprise, business
process matching based on revealing the business processes poses a
clear threat to privacy, as it may expose sensitive information about
the inner operation of the enterprises.

In this talk we propose a solution to this problem for business processes described by means of service automata. We propose a measure for similarity between service automata and use this measure to devise an algorithm that constructs the most similar automaton to the first one that can interoperate with the second one. To achieve privacy, we implement this algorithm on the Sharemind platform for secure multiparty computation. As a result, only the correction information is leaked to the first enterprise and no more.

This is joint work with Dilian Gurov and Roberto Guanciale, appeared at PST 2015.

Slides from the talk [pptx]

*Abstract*: We consider the problem of minimizing the
communication in single-database private information retrieval
protocols in the case where the length of the data to be transmitted
is large. We present first rate-optimal protocols for
1-out-of-*n* computationally private information retrieval
(CPIR), oblivious transfer (OT), and strong conditional oblivious
transfer (SCOT). These protocols are based on a new optimalrate
leveled homomorphic encryption scheme for large-out putpolynomial-size
branching programs, that might be of independent interest. The
analysis of the new scheme is intricate: the optimal rate is achieved
if a certain parameter *s* is set equal to the only positive root
of a degree-*(m + 1)* polynomial, where *m* is the length of
the branching program. We show, by using Galois theory, that even when
*m* = 4, this polynomial cannot be solved in radicals. We employ
the Newton-Puiseux algorithm to find a Puiseux series for *s*,
and based on this, propose a *Θ (log m)*-time algorithm to
find an integer approximation to *s*.

This is joint work with Aggelos Kiayias, Nikos Leonardos, Kateryna Pavlyk and Qiang Tang. It appeared in PoPETs.

Slides from the talk [pdf]

*Abstract:* Oriented coloring is a coloring of the vertices of
an oriented graph such that: (1) no two neighbors have the same color,
(2) if there is an arc directed from the color *a* to *b*,
then no arc is directed from *b* to *a*. In this talk, I
will present a work in progress about the bounds on the oriented
chromatic of rectangular grids. Moreover, I will describe an integer
program which finds oriented colorings of grids.

This is joint work with Bahman Ghandchi and Dirk Oliver Theis.

Slides from the talk [pdf]

*Abstract:* Benchmark results for solving a differential
equation using the Fourier Transform are reported on a variety of
supercomputers. They show that total on chip bandwidth is a very good
performance indicator until network communication costs dominate. For
large data problems, similar benchmarks may be useful in indicating
what kind of computing system to use. A discussion of some of the
computational cost estimation and possibilities for extension will be
made.

This is joint work with S. Aseeri, O. Batrašev, M. Icardi, B. Leu, A. Liu, N. Li, E. Müller, B. Palen, M. Quell, H. Servat, P. Sheth, R. Speck, M. Van Moer, J. Vienne.

Slides from the talk [pdf]

*Abstract:* In our previous works, we presented a generic
method for turning passively secure protocols into protocols secure
against covert attacks, adding an offline preprocessing and a cheap
post-execution verification phase. One problem of our method was that
it has protected honest parties from dishonest parties only, but not
from other honest parties. In this work, we propose a varaint of
universal composability model that protects honest parties from other
honest parties. We modify our verification protocol in such a way that
the honest parties are no longer afraid of leaking their secrets to
other honest parties.

This is joint work with Peeter Laud.

Slides from the talk [pdf]

*Abstract:* We consider how to perform privacy-preserving
analyses on private data from different data providers and containing
personal information of many different individuals. We combine
differential privacy and secret sharing based secure multiparty
computation in the same system to protect the privacy of both the data
providers and the individuals. We have implemented a prototype of this
combination and have found that the overhead of adding differential
privacy to secure multiparty computation is small enough to be usable
in practice.

This is joint work with Peeter Laud, accepted to ACSAC 2015.

Slides from the talk [pdf]

*Abstract:* The *rectangle covering number* of an
*n × n* Boolean matrix *M* is the smallest number of
1-rectangles which are needed to cover all the 1-entries of *M*.
The concept is an important lower bound in Communication Complexity
and Combinatorial Optimization. It is also known as the
*Boolean rank* of *M*: the smallest *k* such
that *M* is the product of an *n × k* and a
*k × n* matrix under Boolean arithmetic (1+1 = 1). Under
the name of \textit{biclique covering number} of a bipartite graph,
the concept is important in graph theory and algorithmics.

By a construction of Lovász and Saks, the rectangle covering number
is the chromatic number of a graph constructed from *M*: The
Lovász-Saks matrix-graph *Graphd(M)* has as its vertex set the
set of pairs
*(k,l)* with *M _{k,l}*=1, and two
vertices

In our paper, we study the rectangle covering number of random
*n × n* matrices, where each entry is 1 with
probability *p*, and the entries are independent. As usual, we
are interested in *n → ∞* and *p* is allowed
to vary with *n*. To bound the rectangle covering number, i.e.,
the chromatic number of the Lovász-Saks graph, we also study its
clique number (cliques are called "fooling sets" in communication
complexity vernacular and "sets of independent entries" in matrix
theory) and its independence number.

This is joint work with Dirk Oliver Theis.

Slides from the talk [pdf]

*Abstract*: Sharemind is an efficient framework for secure
multiparty computations (SMC). Its efficiency is in part achieved
through a large set of primitive, optimized SMC protocols that it
makes available to applications built on its top. The size of this set
has brought with it an issue not present in frameworks with a small
number of supported operations: the set of protocols must be
maintained, as new protocols are still added to it and possible
optimizations for a particular sub-protocol should be propagated into
larger protocols working with data of different types.

To ease the maintenance of existing and implementation of new protocols, we have devised a domain-specific language (DSL) and its optimizing compiler for specifying protocols for secure computation. In this talk, we give the rationale of the design, describe the translation steps, the location of the compiler in the whole Sharemind protocol stack, and the results obtained with this system.

This is joint work with Peeter Laud, accepted to CCS 2015.

Slides from the talk [pdf]

*Abstract:* Extremal graph theory studies among other things
the following question. For a given number *n*, what is the
*maximum* number of edges in an *n*-vertex graph that
contains no copy of a fixed subgraph, such as a triangle, or 4-cycle,
or any other. Here by a subgraph, we do not necessarily mean an
induced subgraph, so for example the complete graph on 4 vertices will
contain the 4-cycle as a subgraph. You could also ask about the
*minimum* number of edges in a triangle- or 4-cycle- etc. free
graph, with the property that upon adding an arbitrary edge to it, we
necessarily create a triangle or 4-cycle etc. This maximum is known as
the extremal or Tur'an number *ex(n, H)*, whereas this minimum is
known as the saturation number *Sat(n,H)* where *H* is the
forbidden subgraph. We study the game version of these two numbers,
which is sort of an average of the two -- we study it in this and some
related contexts. I will talk about early work, our results and
outline some strategies for the players in different games.

This is joint work with Jonathan D. Lee.

Slides from the talk [pdf]

*Abstract*: One of the most promising candidates for universal
and scalable quantum computing is linear optics with single photon
sources and detectors. It is universal because any unitary operator
can be implemented by a sequence of beam splitters and phase shifters
acting on a suitable number of modes. It is scalable when implemented
as a photonic integrated circuit.

In this talk, I will describe some general ideas for constructing linear optical quantum circuits using unitary matrix decompositions. In particular, I will describe recursive schemes for quantum Fourier transforms and the inversion about the mean in Grover's algorithm.

Slides from the talk [pdf]

*Abstract*: Residual finite state automata (RFSA) are a subclass
of nondeterministic finite automata with the property that every state
of an RFSA defines a residual language (a left quotient) of the
language accepted by the RFSA. Every regular language has a unique
canonical RFSA which is a minimal RFSA accepting the language. We
study the relationship of RFSAs with atoms of regular languages. We
generalize the double-reversal method of finding a canonical RFSA,
presented by Denis, Lemay, and Terlutte.

This work was presented at DCFS 2015.

Slides from the talk [pdf]

*Abstract*: In the Haskell community, there is a controversy
about what the laws of the MonadPlus type constructor class ought to
be. We suggest that there is no single universal correct answer,
however there is a universal method. Important classes of notions of
finitary nondeterminism are captured by what we call monads of
semigroups and monads of monoids, but also by monads of different
specializations of semigroups and monoids. Some of these
specializations of monads are exotic and amusing too.

Slides from the talk [pdf]

*Abstract:* In this paper we address the problem of large
space consumption for protocols in the Bounded Retrieval Model (BRM),
which require users to store large secret keys subject to adversarial
leakage. We propose a method to derive keys for such protocols
on-the-fly from weakly random private data (like text documents or
photos, users keep on their disks anyway for non-cryptographic
purposes) in such a way that no extra storage is needed. We prove
that any leakage-resilient protocol (belonging to a certain, arguably
quite broad class) when run with a key obtained this way retains a
similar level of security as the original protocol had. Additionally,
we guarantee privacy of the data the actual keys are derived
from. That is, an adversary can hardly gain any knowledge about the
private data except that he could otherwise obtain via leakage. Our
reduction works in the Random Oracle model.

As an important tool in the proof we use a newly established bound
for min-entropy, which can be of independent interest. It may be
viewed as an analogue of the chain rule -- a weaker form of the
well-known formula H*(X* | *Y)* = H*(X,
Y)* - H*(Y)* for random variables *X*,
*Y*, and Shannon entropy, which our result originates from. For
min-entropy only a much more limited version of this relation is known
to hold. Namely, the min-entropy of *X* may decrease by up to the
bitlength of *Y* when *X* is conditioned on Y, in
short: \widetilde H*(X* | *Y)* ≥
H_{∞}*(X)* - |*Y*|. In many
cases this inequality does not offer tight bounds, and such
significant entropy loss makes it inadequate for our particular
application. In the quasi chain rule we propose, we inject some
carefully crafted side information (spoiling knowledge) to show that
with large probability the average min-entropy of *X* conditioned
on both: *Y* and this side information can be almost lower
bounded by the min-entropy of *(X, Y)* decreased by the
min-entropy of *Y* conditioned on the side information.

This is joint work with Konrad Durnoga, Tomasz Kazana and Maciej Zdanowicz.

Slides from the talk [pdf]

*Abstract*: Multiport switches are commonly used as data
processing and routing devices in computer networks. A network switch
routes data packets between its multiple input and output
ports. Packets from input ports are stored upon arrival in a switch
fabric comprising multiple memory banks. This can lead to memory
contention when distinct output ports request packets from the same
memory bank, resulting in a degraded switching bandwidth. To solve
this problem, switch codes are introduced as a tradeoff between
redundancy and service. Using techniques from combinatorial design and
graph theory, constructions for switch codes serving different types
of requests are given.

This is joint work with Yeow Meng Chee, Fei Gao and Samuel Tien Ho Teo.

Helger Lipmaa

Vitaly Skachek

Tarmo Uustalu

Viimane uuendus 9.10.2015