18th Estonian Winter School in Computer Science (EWSCS)
XVIII Eesti Arvutiteaduse Talvekool

Palmse, Estonia, March 3 - 8, 2013

Student Talks 2013 (abstracts)

Multisorted Algebras and Refined Notions of Computation

Danel Ahman
Tallinn University of Technology, Dept. of Computer Science/
University of Edinburgh, School of Informatics, UK, Estonia

In seminal work, Moggi proposed the use of strong monads to model computational effects (what he called notions of computations) in programming languages. Later, Plotkin and Power showed that a wide range computational effects can be identified with algebraic theories whose free algebras determine the monads proposed by Moggi.

This talk is about the first steps in our work of investigating more refined notions of computation by studying the combination of refinement types and algebraic theories of computational effects. In particular, I will be walking the audience through a small motivating example of global state where every location can be switched both on and off (and also equipped with specific permission requirements). This example illustrates step-by-step the generalizations we have made to the conventional algebraic theories and also indicates why the conventional single-sorted approach does not seem to suffice.

(Joint work with Gordon Plotkin and Alex Simpson.)

A More Efficient Protocol Suite for Secure Multiparty Computation

Dan Bogdanov
Cybernetica AS, Estonia

In 2008, we proposed a secure multiparty computation protocol suite that was built around efficient addition and multiplication protocols. All other operations like bit extraction, comparison and equality were derived from these two. In our recent paper, we present a new suite of protocols that is significantly more efficient, but makes more assumptions on the deployment of the system. We were able to make the equality check several orders of magnitude faster than in the earlier protocol suite. The talk will give an overview of the tradeoffs and results of the optimizations.

Certified Normalization of Context-Free Grammars

Denis Firsov
Institute of Cybernetics at TUT, Estonia

Several decision procedures for context-free grammars work on grammars in some normal form. The aim of this work was to implement verified conversions between context-free grammars in general and normal forms. This was done by implementing and verifying correctness of four transformations in the Agda dependently typed programming language. These transformations can be applied independently, giving different versions of the original grammar. When all four of them are applied in the right order, then the Chomsky normal form is achieved.

The transformations were proved to be sound and complete. Soundness and completeness state that parse trees for the normalized grammar and parse trees for the original grammar are interconvertible. Since the proofs are constructive, they are in fact certified parse tree conversion programs. (Joint work with Tarmo Uustalu.)

A New Way to Protect Privacy in Large-Scale Genome-Wide Association Studies

Liina Kamm
Cybernetica AS, Estonia

Increased availability of various genotyping techniques has initiated a race for finding genetic markers that can be used in diagnostics and personalized medicine. Although many genetic risk factors are known, key causes of common diseases with complex heritage patterns are still unknown. Identification of such complex traits requires a targeted study over a large collection of data. Ideally, such studies bring together data from many biobanks. However, data aggregation on such a large scale raises many privacy issues. We show how to conduct such studies without violating privacy of individual donors and without leaking the data to third parties. The presented solution has provable security guarantees.

Fast Probabilistic File Fingerprinting for Big Data

Konstantin Tretjakov
University of Tartu, Inst. of Computer Science, Estonia

Biological data acquisition is raising new challenges, both in data analysis and handling. Not only is it proving hard to analyze the data at the rate it is generated today, but simply reading and transferring data files can be prohibitively slow due to their size. This primarily concerns logistics within and between data centers, but is also important for workstation users in the analysis phase. Common usage patterns, such as comparing and transferring files, are proving computationally expensive and are tying down shared resources.

We present an efficient method for calculating file uniqueness for large scientific data files, that takes less computational effort than existing techniques. This method, called Probabilistic Fast File Fingerprinting (PFFF), exploits the variation present in biological data and computes file fingerprints by sampling randomly from the file instead of reading it in full. Consequently, it has a flat performance characteristic, correlated with data variation rather than file size. We demonstrate that probabilistic fingerprinting can be as reliable as existing hashing techniques, with provably negligible risk of collisions. We measure the performance of the algorithm on a number of data storage and access technologies, identifying its strengths as well as limitations.

Probabilistic fingerprinting may significantly reduce the use of computational resources when comparing very large files. Utilisation of probabilistic fingerprinting techniques can increase the speed of common file-related workflows, both in the data center and for workbench analysis. The implementation of the algorithm is available as an open-source tool named pfff, as a command-line tool as well as a C library.

A formalization of the Max-flow Min-cut Theorem in Higher Order Logic

Niccol├▓ Veltri
Institute of Cybernetics at TUT, Estonia

We present a formalization of the Max-flow Min-cut theorem in HOL Light. The Max-flow Min-cut theorem is a major result in graph theory and an application of the strong duality theorem in linear programming. We formalize a graph-theoretical version of the proof of this theorem. The formalization is nontrivial not only for the complexity of this mathematical proof per se, but also because of the lack of a basic library for graphs in the standard repositories of HOL Light.

Valid CSS! Valid XHTML 1.0 Strict Last changed November 26, 2014 19:55 EET by local organizers, ewscs13(at)cs.ioc.ee
EWSCS'13 page: http://cs.ioc.ee/ewscs/2013/