Ettekande slaidid. [ppt]

*Abstract:* Quantum walks are quantum counterparts of random
walks. In the last 5 years, they have become one of main methods of
designing quantum algorithms. Quantum walk based algorithms include
element distinctness, spatial search, quantum speedup of Markov
chains, evaluation of Boolean formulas and search on "glued trees"
graph. In this talk, I will describe the quantum walk method for
designing search algorithms and show several of its applications.

Ettekande slaidid. [pdf]

*Abstract:* A very simple and well-known example of a question
answering system is an information system in the sense of Z. Pawlak,
known also as a knowledge representation system, attribute system, Chu
space, formal many-valued context etc. A determined, or complete,
information system is a quadruple *I := (Q, A, V, F)*, where
*Q* is as set of objects, *A* is a set of their attributes,
*V* is an *A*-indexed family of sets (*V _{a}*
is the set of values for the attribute

In the talk, more general question answering systems, which may be non-complete and may admit built-in inclusion or/and functional dependencies between questions, will be dealth with. I shall report several results concerning the algebraic structure of such systems, and discuss the problem whether an arbitrary question answering system can be simulated by a complete Pawlak's system.

Ettekande slaidid. [ppt]

*Abstract:* Topological image features such as ridges and
valleys provide an intuitive and powerful way of characterizing image
content. The notion of ridges and valleys in digital images was
introduced by Haralick already in 1983, but so far it has received
fairly limited attention. The main reason is the lack of efficient
and robust algorithms for their computation in discrete images.

Typically lines and edges are detected using Sobel or Laplace operators; however, they significantly suffer from noise and provide disconnected or thick lines. Serious post-processing such as gap filling or skeletonization is required. Topological formulation of lines as ridges or valleys of a 3D surface overcome these limitations in an elegant way. Ridges are not sensitive to changes in contrast or brightness of the image and are less sensitive to noise leading to superior applicability.

In this talk we review image topological feature extraction methods and give an efficient simple and robust algorithm for their computation in discrete images. We discuss the performance and characteristics of the new algorithm on practical examples and show its benefits over traditional approaches. Therefore the way to using the image topological features is open for widespread use. (Joint work with Paulis Kikusts.)

Ettekande slaidid. [ppt]

*Abstract:* A. Ambainis and R. Freivalds proved in 1998 that
for recognition of some languages the quantum finite automata can have
smaller number of the states than deterministic ones, and this
difference can even be exponential. The proof contained a slight
non-constructiveness, and the exponent was not shown explicitly. For
probabilistic finite automata exponentiality of such a distinction was
not yet proved. The best (smaller) gap was proved by Ambainis in
1996. The languages considered by Ambainis/Freivalds were presented
explicitly but the exponent was not. In a very recent paper by
R. Freivalds the non-constructiveness is modified, and an explicit
(and seemingly much better) exponent is obtained at the expense of
having only non-constructive description of the languages
used. Moreover, the best estimate proved in this paper is proved under
assumption of the well-known Artin's Conjecture (1927) in Number
Theory. The paper contains also a theorem that does not depend on any
open conjectures but the estimate is worse, and the description of the
languages used is even less constructive. This seems to be the first
result in finite automata depending on open conjectures in Number
Theory.

There was a never published "folk theorem" proving that quantum
finite automata with mixed states are no more than super-exponentially
more concise than deterministic finite automata. It was not known
whether the super-exponential advantage of quantum automata is really
achievable. A new result by R. Freivalds uses a novel proof technique
based on Kolmogorov complexity to prove that there is an infinite
sequence of distinct integers n such that there are languages
*L _{n}* in a 4-letter alphabet such that there are
quantum finite automata with mixed states with

Ettekande slaidid. [pdf]

*Abstract:* tba

Ettekande slaidid. [pdf]

*Abstract:* Bi-intuitionistic logic is the extension of
intuitionistic logic with exclusion, a connective dual to
implication. Bi-intuitionistic logic was introduced by Rauszer as a
Hilbert calculus with algebraic and Kripke semantics. But her
subsequent "cut-free" sequent calculus has recently been shown by
Uustalu to fail cut-elimination.

We propose a new sequent calculus for bi-intuitionistic logic which sits somewhere between display calculi and traditional sequent calculi by using nested sequents. Our calculus enjoys a simple (purely syntactic) cut-elimination proof as do display calculi. But it has an easily derivable variant calculus which is amenable to automated proof search as are (some) traditional sequent calculi. As far as we know, our new calculus is the first sequent calculus for bi-intuitionistic logic which uses no semantic additions like labels, which has a purely syntactic cut-elimination proof, and which can be used naturally for backwards proof-search. (Joint work with Rajeev Goré and Alwen Tiu.)

Ettekande slaidid. [ppt]

*Abstract:* Euler's investigations of Graeco-Latin squares,
particularly his 36 officer problem can be considered as the start of
the combinatorial design theory. Most actively it developed in the
second half of the 20th century. Essentially it deals with forming a
finite amount of sets from a finite amount of elements, so that
elements are distributed in sets regularly, in some sense.

Then, in quantum information theory appeared a need for several
vector configurations (in the complex *n*-dimensional space) with
in some sense regular properties. Not only combinatorial designs could
partly help to construct such configurations, but G. Zauner in 1999
showed that these vector configurations are natural generalizations of
combinatorial designs, so can be rightfully called quantum
designs.

A typical example of such quantum design is a system of mutually unbiased bases (MUB). In this talk we will shortly review the current progress in the construction of MUBs and some other quantum designs, and present some new ideas that could help to prove either positive, or negative results in this area. (Joint work with Aleksandrs Belovs.)

Ettekande slaidid. [pdf]

*Abstract:* A common way to specify secure information flow in
a program is non-interference which means that secret inputs in a
program must not influence the public outputs. Jif is an extension of
Java programming language that statically checks the validity of
security annotations. This way it ensures that the program compiles
only if it is non-interferent. We investigate how to model type
systems for computationally secure information flow in Jif. In
particular, we consider a type system proposed by Laud and Vene which
can handle encryption keys as first-class data. We describe how typing
decisions of Laud-Vene type system can be captured using Jif's
declassification mechanism. Also we present a Jif class for "keys" to
encapsulate all necessary information release. (Joint work with Peeter
Laud, to be presented at NordSec 2008).

Ettekande slaidid. [pdf]

*Abstract:* In this paper we introduce a set of computation
rules to determine the attacker's exact expected outcome based on a
multi-parameter attack tree. We compare these rules to a previously
proposed computational semantics by Buldas et al. and prove that our
new semantics always provides at least the same outcome. A serious
drawback of our proposed computations is the exponential
complexity. Hence, implementation becomes an important issue. We
propose several possible optimisations and evaluate the result
experimentally. Finally, we also prove the consistency of our
computations in the framework of Mauw and Oostdijk and discuss the
need to extend the framework. (Joint work with Jan Willemson, to be
presented at IS 2008.)

Ettekande slaidid. [pdf]

*Abstract:* The universally composable cryptographic library
by Backes, Pfitzmann and Waidner provides Dolev-Yao-like, but
cryptographically sound abstractions to common cryptographic
primitives like encryptions and signatures. The library has been used
to give the correctness proofs of various protocols; while the
arguments in such proofs are similar to the ones done with the
Dolev-Yao model that has been researched for a couple of decades
already, the conclusions that such arguments provide are
cryptographically sound.

Various interesting protocols, for example e-voting, make extensive use of primitives that the library currently does not provide. The library can certainly be extended, and in this talk we show how to add threshold homomorphic encryption to the universally composable cryptographic library and demonstrate its usefulness by (re)proving the security of a well-known e-voting protocol. (Joint work with Long Ngo, to be presented at ProvSec 2008.)

Ettekande slaidid. [pdf]

*Abstract:* In this presentation, we review some classical
cryptographic problems and their alternative formulation as matrix
games. The alternative formulation allows us to give a single generic
answer for many problems at once. Namely, we can state several
combinatorial lemmas that provide security guarantees simultaneously
to many primitives, such as commitments, knowledge-extraction, generic
signatures and time-stamping.

*Abstract:* We polish a recent cryptocomputing method of Ishai
and Paskin from TCC 2007. More precisely, we show that every function
can be cryptocomputed in communication, linear in the product of
client's input length and the length of the branching program, and
computation, linear in the size of the branching program that computes
it. The method is based on the existence of a communication-efficient
(2,1)-CPIR protocol. We give several nontrivial applications,
including: (a) improvement on the communication of Lipmaa's CPIR
protocol, (b) a CPIR protocol with log-squared communication and
sublinear server-computation by giving a secure function evaluation
protocol for Boolean functions with similar performance, (c) a
protocol for PIR-writing with low amortized complexity, (d) a
selective private function evaluation (SPFE) protocol. We detail one
application of SPFE that makes it possible to compute how similar is
client's input to an element in server's database, without revealing
any information to the server. For SPFE, we design a 4-message
extension of the basic protocol that is efficient for a large class of
functionalities.

Ettekande slaidid. [pdf]

*Abstract:* It has been known for quite some time that
collision-resistance of hash functions does not seem to give any
actual security guarantees for unbounded hash-tree time-stamping,
where the size of the hash-tree created by the time-stamping service
is not explicitly restricted. We study the possibility of showing that
there exist no blackbox reductions of unbounded time-stamping schemes
to collision-free hash functions. We propose an oracle that is
probably suitable for such a separation and give strong evidence in
support of that. However, the problem of separation still remains
open. We introduce the problem, give a construction of the oracle,
relative to which there seems to be no secure time-stamping schemes
but there still exists a collision-free function family. Although we
rule out many useful collision-finding strategies (relative to the
oracle) and the conjecture seems quite truthful after that, there
still remains a possibility that the oracle can be abused by some very
smartly constructed wrappers. We also argue why it is probably very
hard to give a correct proof for our conjecture. (Joint work with Ahto
Buldas, to be presented at ProvSec 2008.)

Ettekande slaidid. [pdf]

*Abstract:* Python is a very powerful high-level programming
language that is especially suitable for proto-type software
development - this is what scientific computing is often all
about. Within the last 10 years many tools have been developed for
Python to carry out various scientific computing tasks. In this
presentation I'll give a short overview of the tools like F2Py and
SciPy that are often used for numerical computations and comment on
the attempts to implement Computer Algebra Systems to perform some
analytical computations within Python.

Ettekande slaidid. [pdf]

*Abstract:* We show how to use type-level primitive recursion
to implement more general polymorphism than is available in statically
typed languages where polymorphic functions are required to have a
type in the type system. We relax this requirement. This allows us to
define all polymorphic functions for which the result type is a
primitive recursive function of the argument type (actually even more
general, but still total, functions are allowed). These functions do
not have an (explicit) type in the type system (since the equality of
two primitive recursive functions is undecidable) but they can be
viewed to have an implicit type outside the type system.

We also have higher-order type level functions and this combined with primitive recursion allows to define more than just primitive recursive functions, e.g. Ackermann function (which is not primitive recursive) can be defined. The class of definable functions on types is similar to the class of definable functions (on values) in strong functional programming.

We have a static typecase construct, which allows to write these functions as easily as in a dynamically typed language with typecase (e.g. typecases can be used inside any data-level expression, not only in type-level expressions) but our typecases are resolved statically, not at run time. Thus we can always determine the result type of the function from the argument type statically, without any need for dynamic typing.

We also show how this is implemented in Fumontrix, a functional language I created and implemented for my master thesis.

We compare our approach to Haskell (GHC) type classes, multi-stage programming, strong functional programming, and languages with dynamic typecase.

Ettekande slaidid. [pdf]

*Abstract:* Projects like jMock and Hibernate Criteria Query
introduced embedded DSLs into Java. We describe two case studies in
which we develop embedded typesafe DSLs for building SQL queries and
engineering Java bytecode. We proceed to extract several patterns
useful for developing typesafe DSLs for arbitrary domains. Unlike most
previous Java DSLs we find that mixing the Fluent Interface idiom with
static functions, metadata and closures provides for a better user
experience than pure method chaining. We also make very liberal use of
the Java 5 Generics to improve the type safety properties of the
DSLs. (Joint work with Jevgeni Kabanov.)

Ettekande slaidid. [ppt]

*Abstract:* A dependency graph is a structure containing the
operations performed in a program, and dependencies (both data and
control flow) between them. Till now, the dependency graphs are mostly
used in program analysis performed by the optimizing
compilers. However, the dependency graphs can also be successfully
applied for the security protocols analysis. The method is based on a
game involving the adversary and the dependency graph, such that
during that game the adversary gets at least as much information as if
she were listening to / tampering with the communication happening
during the protocol executing. Then we perform a series of game
transformations in such a way that the adversary advantage diminishes
only negligibly from game to game. The goal of the transformations is
to obtain a game, in which the adversary has no advantage at all.

In this talk, we, after a brief introduction to all the stages of the dependency graph-based protocol analysis, summarize the improvements made to our theory over the last year:

- improvements to the dependency graph execution semantics needed for protocol integrity (correspondence) analysis;
- formal definition of a game transformation through graph rewriting;
- practical results achieved.

(Joint work with Peeter Laud.)

Ettekande slaidid. [pdf]

*Abstract:* I will demonstrate a simple and robust program
transformation technique that can automagically improve asymptotic
complexity (e.g., produce a linear-time list reversal function from
the obvious quadratic one). In our version, it applies to monadic
datatypes and can be stated in two flavours, through a datatype
representation with an explicit ("frozen") *bind* constructor and
a special associated defining clause for the
*fold* function and in a functional form with a special
definition of the *bind* function in terms of *build*. The
technique explicates, systematizes, combines and scales a number of
ideas known from the literature, achieving a new level of
generality.

Ettekande slaidid. [pdf]

*Abstract:* Extending our previous work on inductive
representation of cyclic data structures, we look at cyclic sharing
data structures such as term graphs. We propose a de Bruijn like
inductive representation (in Haskell implemented via nested data types
and generalized algebraic data types) supporting principled
programming and reasoning. (Joint work with Makoto Hamana and Tarmo
Uustalu.)

Peeter Laud

Helger Lipmaa

Tarmo Uustalu

Varmo Vene

Viimane uuendus 8.10.2008