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 (Va is the set of values for the attribute a), and F is an A-indexed family of functions (valuations) Fa of type Q → Va. Elements of Q could be reinterpreted as states of I, those of A, as questions that can be put to I, and those of Va, as possible answers to the question a.
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 Ln in a 4-letter alphabet such that there are quantum finite automata with mixed states with 2n + 1 states recognizing the language Ln with probability 3/4 while any deterministic finite automaton recognizing Ln needs to have at least eO(n ln n) states.
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:
(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.)