Jerzy Karczmarczuk (U Caen): Differential algebra in functional sauce

Ettekande slaidid. [pdf]

Abstract: We present a purely functional implementation of two standard -- direct and inverse -- modes of the Automatic Differentiation techniques, permitting to compute the derivatives of expressions within a _numerical_ program exactly and inexpensively. The direct method is based on the overloading of the aritmetic operations to lazy infinite streams, which implement numerical expressions together with _all_ their derivatives, and which realize a closed differential algebra. The reverse method relies on a paradoxal State Monad version in which the "time goes backwards", and the "state" which model the adjoints (derivatives) of intermediate expressions propagates from the future towards the past, exploiting again the laziness of the used language, Haskell. [No previous knowledge of Monads is assumed].

Jerzy Karczmarczuk (U Caen): Implementing quantum abstractions

Ettekande slaidid. [pdf]

Abstract: While 'states' in Quantum Theory are abstract vectors in Hilbert spaces, and observables are abstract operators, all _concrete_ computations need implementable representations thereof. Computer scientists introduce thus "quantum registers", play with concrete matrices, etc., in order to be able to do standard calculi thereupon. One undesirable consequence of such an approach is that _too much_ information is attributed to 'quantum' entities, and the computational model represents not only the system, but also its concrete view. We attempt at implement almost directly the quantum abstractions, keeping the bridge between computations and theoretical physics as short as possible. State vectors are _functions_, operators are higher-order functions, etc. Despite this, very high, level of abstraction, we show how to perform some classic "quantum computations", such as the Deutsch algorithm, or a qubit teleporting. But our formalism is pretty general, applicable to other systems than qubits; we sketch thus also some other application of the presented framework, such as the construction of some concrete wave functions, or the development of lazy perturbational schemes. The talk assumes a _rudimentary_ knowledge of quantum mechanics.

Adam Eppendahl: Uniformity for program semantics

Abstract: As a notion of uniformity, the definition of natural transformation in category theory serves ordinary mathematics well. The mathematics of program semantics, which uses higher order constructions of mixed variance, seems to require something else. Exactly what is still unknown. A few examples illustrate the troubles and triumphs of various definitions.

Meelis Kull: Speeding up clustering

Ettekande slaidid. [pdf]

Abstract: Gene expression data clustering methods group together similar genes. We have developed a method that avoids calculations of all-against-all distances, yet identifies rapidly most of the similar gene pairs. Using this method we have developed fast approximate versions of single-, average-, and complete-linkage hierarchical clustering. (Joint work with Jaak Vilo.)

Ago Kuusik: The ILP approach to the layered graph drawing

Ettekande slaidid. [pdf]

Abstract: It is generally believed that a drawing of a graph is clearly understandable and aesthetically pleasing, if the drawing contains as few edge crossings as possible. A special case of general drawing of a directed graph is the layered drawing where the vertices of the graph are distributed between discrete layers so that all the edges of the graph point to the same direction. The edge crossing minimisation in such a drawing is an NP-hard combinatorial optimisation problem. A close alternative to that - the extraction of the maximum level planar subgraph is equally difficult. We attempt to solve these problems using the Integer Linear Programming approach (ILP). The ILP technique can be regarded as "a way between" imprecise fast heuristic algorithms and exponential-time exact algorithms, allowing to achieve close to optimal results in "acceptable time". We explain the ILP approach in general and talk about the specifics of solving the two aforementioned graph drawing problems by the ILP.

Kristo Käärmann: Inferring parental genomes from offspring's DNA

Ettekande slaidid. [pdf]

Abstract: Every cell possesses two independent copies of DNA, one from the female parent and the other from the male. Modern biotechnology is not yet capable of reading the sequence from a particular one of those two helices, but produces a succession of unordered pairs of values (eg {A,G},{G,G},{T,C},...) as genotyping output. At a considerable computational expense, mathematical methods can be exploited to reconstruct genes and actual sequences (haplotypes) from such raw genotyping data, but for slightly longer genome regions the degrees of freedom quickly become unmanagable for statistical simulations. Knowing the individual haplotypes is often essential for interpreting genetic variance and discovering genome structure.

This talk aims at exhibiting this bioinformatics problem, explaining the underlying mathematical models and proposing a few ideas to tackle the computational issue.

Peeter Laud: Universaalselt komponeeritavast ajatembeldusest

Ettekande slaidid. [ps.gz]

Kokkuvõte: Universaalne komponeeritavus on krüptograafiliste süsteemide turvadefinitsioonide omadus, mis lubab komponeeritud süsteemide omaduste üle arutlemise taandada nende komponentsüsteemide ideaalsete funktsionaalsuste üle arutlemisele; komponentsüsteemide realisatsioonide iseärasusi pole tarvis arvesse võtta. Ajatemplisüsteemid on krüptograafilised süsteemid, mis lubavad osapooltel fikseerida bitijadade loomise (täpsemalt öeldes: ajatembeldamise) järjekorra, vajamata selleks usaldatud osapooli. Käesolevas ettekandes uurime erinevaid võimalusi ajatemplisüsteemide turvalisuse universaalselt komponeeritavate definitsioonide andmiseks ning arutleme, milliseid kompromisse sealjuures teha tuleb.

Sven Laur: Privaatne otsing: indeksid ning alternatiivid

Ettekande slaidid. [pdf]

Kokkuvõte: Ettekanne käsitleb otsinguid üle krüpteeritud andmete. Üheks uudseimaks lahenduseks on Bloomi indeksi kasutamine, idee enda pakkus välja E.-J. Goh artiklis [crypto eprint 2003/216]. Kahjuks pole artiklis toodud turvatõestus korrektne, seetõttu pakume välja alternatiivse paremini struktueeritud lähenemise, mis võimaldab täpselt määratleda kasutavatelt primitiividelt nõutud turvaomadusi. Saavutatud tulemused on üldisemad, kattes kogu mäluta andmestruktuuride klassi. Tuntumateks näideteks sellistest andmestruktuuridest on nimistud ja prefikspuud. Lisaks vaatleme võimalikke laiendusi nagu eristamatud päringud, ligikaudne otsing ja päringute kontroll/piiramine.

Helger Lipmaa: An oblivious transfer protocol with log-squared communication

H. Lipmaa, An oblivious transfer protocol with log-squared communication, draft paper. [crypto eprint]

Ettekande slaidid. [pdf]

Abstract: We propose a family of two-round $1$-out-of-$n$ computationally-private information retrieval protocols for elements from $\mathbb{Z}_d$ that has the next properties: (a) In the asymptotically optimal case, it has communication $\Theta(\log^2 n\cdot {k}+\log n\cdot \log d)$ bits, where ${k}$ is the security parameter; (b) It can be based on an arbitrary IND-CPA secure length-flexible public-key cryptosystem. In particular, the sender-privacy of the new protocols can be based on the assumption that the Decisional Composite Residuosity Problem is hard. The proposed protocols can be transformed to two-round computationally chooser-private and information-theoretically sender-private $1$-out-of-$n$ oblivious-transfer protocols for elements from $\mathbb{Z}_d$, with the same asymptotical communication, that is secure assuming that the underlying cryptosystem is IND-CPA secure, i.e., in the standard model.

Härmel Nestra: Transfinite semantics for program slicing

Ettekande slaidid. [ps.gz]

Abstract: Transfinite semantics are semantics which observe sequences of computation steps continuing beyond the initial enumerable part of it. Transfinite semantics have been the subject of interest mainly for functional languages (due to possible infinite data structures whose components are computed in such an order which does not lead to a completely evaluated term within the least enumerable number of evaluation steps, having however an intuitively clear value being able to be obtained using another order of reduction or --- continuing the actual reduction sequence with transfinite steps).

We are interested in transfinite semantics in the case of imperative languages. This means returning of the control from infinite loops and continuing the computations after that. The reason of studying such semantics is given by program slicing and its well-known "semantic anomaly" which arises in the case of slicing away infinite loops.

Our farther aim is to give a specification of the concept of slicing in terms of transfinite semantics so being independent of the actual syntax of the language. The idea of using transfinite semantics for specifying slicing is not new but it still lacks from a satisfactory realization.

Hendrik Nigul: Approximate string matching using suffix tries

Ettekande slaidid. [pdf]

Abstract: In computational biology approximate string matching is a central problem. Suffix trie data structures are used as they provide concise representation of internal structure of strings enumerating conviently all substrings. We present how to construct suffix tries and how to use them in applications. We mainly focus on finding approximate matches of different patterns in a sequence as well as approximate all-against-all matching.

Tarvo Raudvere: Design and verification in the ForSyDe methodology

Ettekande slaidid. [pdf]

Abstract: The ForSyDe methodology has been developed for system design, where the design flow starts at a high abstraction level. The initial system model in ForSyDe is described as a functional specification model that is synchronous, deterministic and can be executed in the functional language Haskell. The design flow continues with the refinement of the specification model to an implementation model. The refinement is done through a series of applications of well-defined design transformations, which are described in the transformation library. Both the specification and the implementation model are described in the functional domain, which makes it easier to verify the implementation against the specification considering design constraints, since the same verification techniques can be used for both models. The implementation model as a result of the refinement process has all the low-level details required for mapping to hardware (VHDL) and software (C++).

Hellis Tamm: Bideterministic automata and minimal representations of regular languages

Ettekande slaidid. [pdf]

Abstract: Bideterministic automata are deterministic automata with the property of their reversal automata also being deterministic. It has been known that a bideterministic automaton is the minimal deterministic automaton accepting its language. We show that any bideterministic automaton is the unique minimal automaton among all (including nondeterministic) automata accepting the same language. We also present a more general result that shows that under certain conditions a minimal deterministic automaton accepting some language or the reversal of the minimal deterministic automaton of the reversal language is a minimal automaton representation of the language. These conditions can be checked in polynomial time. (Joint work with Esko Ukkonen.)

Tarmo Uustalu: Partiality is an effect

Ettekande slaidid. [pdf]

Abstract: Partial functions are usually considered as something basic or "purely functional" in functional languages, hence semantics starts from CPO-like categories with a fixpoint operator. We maintain that partiality due to non-termination can also be treated as a monadic effect. The appropriate monad is the free completely iterative monad on the identity functor, which captures timed, possibly non-terminating computation; one can also consider the quotient that identifies all terminating computations yielding the same value (constructively, this is not the same as the error monad, which can only capture partiality due to finite failure). Looping constructions are supported immediately; we discuss general recursion and combination of the monad with monads for other effects. (Work in progress jointly with T. Altenkirch and V. Capretta.)

Jüri Vain: On the synthesis of provably correct discrete controllers

Ettekande slaidid. [pdf]

Abstract: Discrete controllers used in embedded systems can be considered as reactive programs with (possibly hard) real time constraints. The parallel composition of the controller(s) and continuous plant has to satisfy certain safety and liveness properties that are formulated in the form of interface specifications. A timed automata based synthesis approach is discussed and the decidability proof of the problem is outlined.

Varmo Vene: Build, augment and destroy, universally

N. Ghani, T. Uustalu, V. Vene. Build, augment and destroy, universally, to appear in Proc. of 2nd Asian Symp. on Programming Languages and Systems, APLAS'04 (Taipei, Nov. 2004).

Ettekande slaidid. [pdf]

Abstract: We give a semantic footing to the 'fold/build' syntax of programming with inductive types, covering shortcut deforestation, based on a universal property. Specifically, we define a semantics for inductive types based on limits of algebra structure forgetting functors and show that it is equivalent to the usual initial algebra semantics. We also give a similar semantic account of the 'augment' generalization of 'build' and of the 'unfold/destroy' syntax of coinductive types. For 'augment', we show that it is definable for a much wider class of inductive types than has previously been recognized. (Joint work with Neil Ghani and Tarmo Uustalu.)

Sven Laur: Krüpto? ... See on imelihtne! (seminar)

Seminari alusmaterjal. [ps.gz]

Kokkuvõte: Enamik krüptograafilisi primitiive ja protokolle on turvalised vaid teatud tingimustel. Seminaris vaatame, mis saab siis, kui need tingimused pole täidetud või kui protokoll "lekib". Seminar ei nõua erilisi eelteadmisi, igaüks võib ennast proovile panna.

Peeter Laud
Helger Lipmaa
Tarmo Uustalu
Varmo Vene
Viimane uuendus 11.10.2004