Ettekande kiled. [pdf]

*Abstract:*
Dataflow variables are concurrent logic variables in the Oz
programming language. These variables are single-assignment, whereas a
thread reading an unbound variable is suspended until the variable is
bound to a value. An unbound variable can be stored to (unified with)
the field of a data structure and sent over the network. These
characteristics simplify and enrich concurrent and distributed
programming. Dataflow variables are closely related to futures and
promises in E and Alice ML programming languages, or M-vars in Haskell
programming language.

Ettekande kiled. [pdf]

*Abstract:*
Interactive seminar.

Ettekande kiled. [pdf]

*Abstract:*
Cellular automata (CA) are synchronous distributed systems where the
next state of each device only depends on the current state of its
neighbors. The global dynamics of configurations can thus be presented
via a finitary function, even when the devices are infinitely many. In
this case, it is of interest to understand whether the local
presentation provides sufficient information for determining whether
the global dynamics has certain properties.

In this talk, aimed at getting people acquainted with CA theory, we will talk about the problem of determining surjectivity (every configuration has AN ancestor) and bijectivity (every configuration has ONE ancestor) of CA from their local presentation. We will present several characterizations of surjectivity and discuss the issues linked to the algorithmic tractability of these problems.

Ettekande kiled. [pdf]

*Abstract:*
In this talk I propose that when doing detailed proofs or formal
developments it is crucial to use convenient representations of data
structures. Otherwise you spend all your time fighting against them. I
will describe what I think is a nice example: a first order
presentation of a function space. This helped to simplify considerably
the formalisation at the core of my thesis: a formal proof of
normalisation for simply-typed lambda calculus. I will also try to
offer some intuition as to why I think this is an indicative of a good
representation and why dependent types are helpful in this
respect.

Ettekande kiled. [pdf]

*Abstract:*
Stably compact spaces arise as an abstractly topological setting for
coherent domains in their Scott topologies. These spaces are typically
$T_0$ spaces. In their work aiming at generalizing Samson Abramsky's
*domain theory in logical form* to the bigger class of coherent
domains, Achim Jung et al introduced the notion of strong proximity
lattice (bounded distributive lattice plus a specific binary relation)
as a stone dual for stably compact spaces. Later on, Mohamed El-Zawawy
and Achim Jung generalized the celebrated Priestley duality of bounded
distributive lattices and totally order-disconnected spaces (Priestley
spaces) to cover strong proximity lattices. This resulted in
introducing the notion of apartness relation on Priestley spaces which
are $T_2$ spaces.

In this talk, I present some results came out of studying the relationship between the $T_0$ class of stably compact spaces and the Hausdorff ($T_2$) class of Priestley spaces equipped with apartness relations. This includes results resulted from studying the relationship between suitable morphisms on the two classes of topology, studying the co-compact topology of stably compact spaces in terms of Priestley spaces, and linking interesting concepts in different sides of dualities mentioned above.

Ettekande kiled. [pdf]

*Abstract:*
This presentation provides experience report in using domain-specific
languages for building information systems. Since 2004, Cybernetica
has developed information systems for Estonian Tax and Customs Board.
During this time we have built three different domain-specific
languages for describing rules for verification of the documents
submitted to the system. These languages make different trade-offs in
terms of succintness, expressive power, ease of use and learning
curve. This presentation discusses these trade-offs in light of our
practical experiences.

Ettekande kiled. [pdf]

*Abstract:*
We give an initial algebra characterisation of cyclic data structures.
We also show that this provides mathematically clean applications in
Haskell: implementation of cyclic data structures by GADTs and a
notation for arrows with loops.

Ettekande kiled. [pdf]

*Abstract:*
We describe the new model of attack tree calculations which is closer
to real-life situations. The model allows attacker to choose the best
order for the elementary attacks and also considers blocking
elementary attacks, which fail the whole attack tree, if they
fail.

Ettekande kiled. [pdf]

*Abstract:*
Modern applications rely heavily on XML to represent data internally
and to interact with other applications and with end users. XSL
transformations are commonly employed to transform between these
representations These XSL transformations need to be updated whenever
the underlying XML formats evolve. We have developed a set of
guidelines to address this maintainability problem. The talk will
discuss ways of measuring stylesheets guidelines conformance.
Additionally, a procedure for tuning non-conformant stylesheets for
greater maintainability will be discussed.

Ettekande kiled. [pdf]

*Abstract:*
The problem of rank aggregation arises if we can study one question
with different methods that provide their results as preference lists
and we want to combine the outcomes to achieve more reliable and
robust answers. The problem is important for example in the context of
information retrieval. In bioinformatics, the rank aggregation problem
also occurs naturally in many applications, since the ordered list of
items is a common result for a database query, similarity search or
statistical analysis. Also the need for data aggregation is strong,
because many data sources can be unreliable. The high level of noise,
however, means that the classical rank aggregation do not work very
well on this setting.

We present an algorithm for rank aggregation specifically designed for the biological setting, where we have put a special emphasis to the statistical robustness. For each item, we compare the the actual ranks with the case where the input lists is random. Using the classical results of non-parametric statistics, we can quantify the difference and order the items according to it. In addition to the aggregated preference list we get the reliability estimation for each element in the list.

Ettekande kiled. [pdf]

*Abstract:*
Scientific measurements often result in multi-dimensional data arrays
which are not very suitable for relational databases. Scientific data
formats such as HDF5 and NetCDF provide a nice alternative. Due to
more natural organization of data arrays, these formats achieve very
fast and convenient data input and output, supporting scientific
computing applications. This presentation gives a short overview of
the scientific data formats and describes our tool TabCDF for
converting between tabular text files and NetCDF.

Ettekande kiled. [pdf]

*Abstract:*
Semantic interoperability is the ability of two or more computer
systems to interpret exchanged information as percieved by the end
users of both systems. This talk first introduces the concept of
semantic interoperability and envisages specific steps to achieve it.
Then some experiments are presented, which involve, both at national
and international scale, analysis of potential interactions between
informations systems presented as Web services. Finally, future
applications emerging from semantic interoperability are discussed.

Ettekande kiled. [pdf]

*Abstract:*
We propose an automatic service composition methodology where, three
levels of composition knowledge are distinguished: user level, logical
level and implementation level knowledge. We use a formalism of
knowledge synthesis in the form of deductive synthesis for
representing the knowledge architectures of our software. We have
implemented our software in a development environment CoCoViLa that
enables composition throughout these three levels. A motivation for
this approach is a need to overcome the complexity of service
composition on very large sets of atomic services we are dealing with
in our application domain. The domain concerns federated governmental
information systems.

Ettekande kiled. [pdf]

*Abstract:*
I will introduce some operational semantics for the While language.
In general, such semantics may be defined inductively or
coinductively: inductively defined semantics admit finite derivation
trees, thus talk about terminating executions of programs;
coinductively defined semantics admits finite as well as possibly
infinite derivation trees, thus can talk about terminating as well as
non-terminating executions. The notion of non-termination is
intuitive, coinductively defined semantics are as simple as
inductively defined semantics; yet reasoning about non-termination
formally raises some interesting issues.

Ettekande kiled. [pdf]

*Abstract:*
We establish a precise framework for proving efficiency bounds for
cryptographic reductions. Such bounds have been studied for about ten
years but the main focus has been the efficiency of the construction
mostly measured by the number of calls to the basic primitive by the
constructed primitive. Our work focuses on the efficiency of the
wrapper construction that builds an adversary for the basic primitive
and has a black-box access to an adversary for the constructed
primitive. We present and prove some general lower bound theorems for
precise reductions. As an example of using the separation results, we
prove that there are no linear-preserving reductions for proving the
security of hash-then-publish time-stamping schemes to the
collision-resistance of the underlying hash function. More precisely,
we show that every such reduction should be at least of power 1.5. The
best known reductions of this kind are quadratic, so the existence of
power 1.5 reductions still remains an open question.

Ettekande kiled. [pdf]

*Abstract:*
Since the explosive growth of the internet in the late 1990s the
volume of information available on this medium has increased
dramatically. One of the biggest challenges we are facing in regards
to information is storing information in a way so that it can be
found, processed, and retrieved in an efficient and effective way.

Some of the most important tools to find information on the internet nowadays are search engines, like Google or Yahoo!. They are indexing any document on the web and making everything searchable via text based search. Unfortunately this approach of indexing everything, from scientific documents, over blogs, newsgroups, directories, private home pages, company image pages and even pure click farms makes the search process less and less effective the more documents are indexed. At the same time, we find ourselves more and more frustrated using these services.

The semantic web has promised a way out of this dilemma, but until today not succeeded. We propose here an approach being a mixture from techniques from agile software development, graph theory, data mining, and a little pragmatic economy as an alternative. As we just started this project I would be very happy about any new ideas, pointers to other research groups, critiques, and of course praise.

Ettekande kiled. [pdf]

*Abstract:*
We consider acts over semigroups that are certain extended automata
where the set of states and the input alphabet are not necessarily
finite. Moreover, the generating sets of acts can have more than one
element, meaning that the extended automata can have more than one
initial state. Formally, let S be a monoid, that is a semigroup
containing an identity element e. A set A is called *a left act
over monoid* S if there is defined an operation
• : S×A→A
which is compatible with the semigroup operation:
(st)•x = s•(t•x) and e•x = x for every
s,t∈S and x∈A. Every (polynomial) equation on A is of the form
s•x = t•y, s•x = t•x or s•x = a, where a
is a fixed element of A (a constant), s, t ∈ S and x, y are variables.
A left S-act A is called *equationally compact* if every system
of polynomial equations (with constants from A) has a solution in A
provided that every finite subsystem has a solution in A. Fixing
certain restrictions to equations we get different generalizations of
equational compactness. Considering congruence classes instead of
equations we get another type of compactness: an S-act is called
*congruence compact* if every filter base consisting of
classess of congruences, has a nonempty intersection. The presentation
discusses relations between different generalizations of equational
compactness.

Ettekande kiled. [pdf]

*Abstract:*
In this talk a methodology for selection of graded security measures
is presented and a prototype implementation in the form of an expert
system is described. This expert system enables a user to select
security measures quickly in a rational way based on the Pareto
optimality computation. The method takes into account the available
resources instead of using only hard constraints prescribed by
security standards. The prototype expert system is presented that
provides a rapid security solution for a class of known information
systems. The prototype uses computationally efficient discrete
dynamic programming method for optimizing resource allocation.
Coarse-grained security is analyzed using a finite number of levels
(security classes) as security metrics.

Ettekande kiled. [pdf]

*Abstract:*
In the judgmental style of formulating logics, one makes a clear
distinction between judgments and propositions. A judgment represents
an object of knowledge and a proof of it allows us to know the object
of knowledge. In contrast, a proposition conveys no knowledge in
itself, but if A is known to be a proposition, we know what counts as
a verification of its truth. As shown by Pfenning and Davies (2001),
the judgmental formualtion lends itself particularly well to the
development of systems of modal logic.

In this talk, I will give an overview of the judgmental formulation of modal logic. We begin by clarifying the notion of judgments and propositions, and then consider how to internalze judgments in such modalities as necessity, possiblity, and lax modality, in a sound and complete way. I will also introduce a few other modalities that were inspired by the judgmental treatment of logic.

Ettekande kiled. [pdf]

*Abstract:*
Bideterministic automata are deterministic finite automata with the
property of their reversal automata also being deterministic. It can
be easily seen that any bideterministic automaton is a minimal DFA.
Bideterministic automata have also been shown to be minimal NFAs with
respect to the number of states as well as transitions. Furthermore,
bideterministic automata are transition-minimal ε-NFAs. We
also consider minimality issues of bideterministic multitape
automata.

Artikkel. [pdf]

*Abstract:*
A survey is presented of works of Grigori Mints from the eighties of
the last century where logic was applied to program synthesis and to
semantics of specification languages. It demonstrates examples of
fruitful application of logic in computing. This shows that Grigori
Mints has left a visible footprint in the Estonian computer
science.

Liina Kamm

Peeter Laud

Helger Lipmaa

Tarmo Uustalu

Varmo Vene

Viimane uuendus 5.02.2009