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