Abstract: We present a specialization of containers to capture the common situation in programming where every position in a datastructure determines a sub-datastructure rooted by that position. Some natural examples of such datastructures are non-empty lists and node-labelled trees, and datastructures with a designated position or focus (zippers). Containers, as introduced by Abbott, Altenkirch and Ghani are a neat representation for a wide class of parameterized datatypes (set functors) in terms of a set of shapes and a set of positions in each shape. They cover lists, streams, various kinds of trees, etc. and can be used as a "syntax" for programming with these datatypes and reasoning about them.
We show that directed containers are no less neat than containers. While containers denote set functors via a fully-faithful functor, directed containers interpret fully-faithfully into comonads. Our main result is that every comonad whose underlying functor is the interpretation of a container is the interpretation of a directed container. So the answer to the question in the title of this talk is: a container is a comonad exactly when it is a directed container.
In this talk I will cover the basics of containers, introduce the notion of directed containers, show some motivating examples and summarize the main results of our work. (Joint work with James Chapman and Tarmo Uustalu, to be presented at FoSSaCS 2012)
Abstract: One of important spatio-temporal data mining tasks is grouping similar trajectories in order to discover frequent patterns in tracked object motion. Frequent trajectory mining has many applications, such as hurricane prediction, city traffic monitoring, animal behaviour explanation. In this talk we will handle this subject as well as developing similarity measures for routes.
Slides of the talk: [pdf]
Abstract: Sharemind is a secure data analysis system based on secret sharing and secure multi-party computation. Given the recent breakthroughs in alternative secure computation techniques like fully homomorphic encryption and driven by the wish to quickly implement new computation protocols, we have upgraded the design of the Sharemind machine and programming languages. This talk will share some of the ideas that inspired the design of Sharemind 3.
Slides of the talk: [pdf]
Abstract: Set membership and range proofs are cryptographic building blocks. Both of these building blocks are Zero-Knowledge proofs. The goal of these proofs is to convince some verifier on the veracity of a statement without revealing any more information besides the validity of the statement. For the case of set membership, the statement is linked to a secret value that a prover has chosen in a public set. His objective is to prove that his secret is indeed in the public set without revealing any more information besides its membership to the set. Range proofs are particular cases of set membership, where the public set is an integer interval.
Set membership and range proofs have several applications. Some of the most important ones are related to the ITU's Child Online Protection (COP) Initiative. Indeed, range proofs (when considering age intervals) can bring a solution to protect children on internet by two means. First, range proofs can be used to forbid children to access adult contents. Secondly, range proofs can protect children from adult predators, by keeping them away from youth's platform such as forums and social networking services.
Abstract: I will describe the relative monad structure of the untyped/typed lambda-terms which captures the notion of parallel substitution. Interestingly, the algebras for these monads are models (evaluators/interpreters/semantics) of the lambda-terms. I will explain the machinery of relative monads and their algebras, and go through the implementations of the lambda-term examples in the programming language Agda.
Abstract: Parsing is a fundamental component of many software pieces. The ultimate goal of our project is to implement a parser generator for context-free languages, which, given a context-free grammar, should be able to provide a parser together with an independently checkable certificate of its correctness.
As a first approximation of our main goal, we implemented a parser generator for regular languages and showed its correctness using the Agda programming language. Specifically, we programmed a transformation of regular expressions into a Boolean-matrix based representation of finite automata. And we proved (in Agda) that a string matches a regular expression if and only if the finite automaton accepts it.
Abstract: The definition of language recognition by quantum finite automata in the case when the language consists of infinite words is somewhat non-trivial because there is no easy way how to consider a measurement after processing an infinite word. However a natural definition is possible based on measure theory developed by E.Borel and the standard definition of language recognition by deterministic and nondeterministic finite automata in the case when the language consists of infinite words developed by R.Buchi.
We prove that Measure-Many finite quantum automata can recognize with probability 1 languages not recognizable by deterministic and nondeterministic finite automata. On the other hand, Measure-Once finite quantum automata can recognize with a bounded error only languages recognizable by deterministic finite automata.
Slides of the talk: [pdf]
Abstract: ProveIt is a semi-automatic prover tool that helps the user make game-based cryptographic proofs by checking whether the specified reduction schema is applicable for the statement in question. The tool is given the formalisation of a security property through a short program also called a game. The user can apply different reduction schemas to the game that is then rewritten according to the applied schema and a new game is obtained. This kind of reduction process assures that the resulting proof is sound. The tool does not perform automatic proofs but rather assists the user in the proof process. This kind of assistance is necessary to help make the tedious and tricky proof validation tractable.
Slides of the talk: [pdf]
Abstract: SecreC is the high-level programming language for expressing privacy-preserving algorithms in the Sharemind framework. The new features of the framework's third version also inspired an overhaul of the language. In this talk, we describe the language and its semantics, and justify the design decisions we made. In Sharemind 3, SecreC will be an imperative language that can polymorphically use various sets of secure computation algorithms. Additionally, the programs in this language satisfy certain information flow security properties.
Abstract: Linear secret sharing is one of the cornerstones of secure multiparty computation. It is common to consider the case where the secret and its shares are field elements. Although this assumption gives a great leverage and allows us to prove many important results, it is also quite restrictive---most common data types used in hardware design and programming are residue rings. In this talk, we discuss which claims still hold if we omit this assumption. In particular, we study a surprising trinity consisting of threshold secret sharing, maximal distance separable codes and arcs. For finite fields, all three terms describe different facets of the same combinatorial object. We show how to extend these definitions to rings without loosing the cherished correspondence.
Abstract: In 2010, Groth constructed the only previously known sublinear-communication NIZK circuit satisfiability argument in the common reference string model. We optimize Groth's argument by, in particular, reducing both the CRS length and the prover's computational complexity from quadratic to quasilinear in the circuit size. We also use a (presumably) weaker security assumption, and have tighter security reductions. Our main contribution is to show that the complexity of Groth's basic arguments is dominated by the quadratic number of monomials in certain polynomials. We collapse the number of monomials to quasilinear by using a recent construction of progression-free sets.
Abstract: In this talk, I will examine alternative definitions of streams being finitely red. These definitions are organized into a hierarchy including also some well-known alternatives in intuitionistic analysis. The hierarchy collapses classically, but is intuitionistically of strictly decreasing strength. The differences in strength are characterized in a precise way by weak instances of the Law of Excluded Middle. (Joint work with Marc Bezem and Tarmo Uustalu)
Abstract: Special purpose languages have been developed over the years to guarantee confidentiality or integrity of data. In practice, the impact of these languages has been limited. Rather than producing new languages from scratch, it has been shown that confidentiality and integrity policies can be also guaranteed via a library, which makes this technology more likely to be adopted. This talk seeks to describe the principles behind security libraries to provide confidentiality and integrity of data in Haskell. The talk will also present the state-of-the-art on security libraries and the main challenges ahead to take this technology into practice. The talk is based on a series of recently published papers.
Abstract: ABS is a modelling language that is designed to be executable. We are working on a new back-end for ABS, utilizing the programming language Scala, that would allow true distributed execution of ABS models. The concurrency model of ABS is two-layer: we have concurrent object groups which communicate with only asynchronous messages and futures (reminiscent of actors) and inside those object groups we have individual objects which use cooperative multitasking. This is very different from the concurrency model of Scala, and thus poses some interesting problems for our compiler. We present the first steps in formalising our approach to compiling ABS code to Scala: we look at the cooperative multitasking inside one COG and show how that can be implemented using delimited continuations, and proceed to show the correctness of this approach.
Slides of the talk: [pdf]
Abstract: We talk about the Advanced Encryption Standard (AES) block cipher implementation on the Sharemind framework. Sharemind is a practical secure multi-party computation framework based on secret sharing. In our AES implementation both plaintext and cipher keys are secret shared among many computing parties. We give an overview of the parallelization techniques used together with the corresponding benchmarking results.
Abstract: The ABS language has a Haskell-style module system. It is possible to specify names of types and functions to be exported, but not types. Therefore it is impossible to typecheck each module separately. In addition, in the ABS language there are no abstract types (also known as opaque types), which are useful for hiding implementation.
In my master's thesis, a module system (supporting separate compilation and abstract types) and a language based on ABS is designed and a type system given for it. The language has explicitly typed imports and exports, sufficient for typechecking each module individually. Safety is then proved for the type system.
This talk presents the key points of my master's thesis: background on ABS separate compilation, overview of our work, a brief overview of our type system, a brief glimpse into the soundness proof.
Abstract: We defined a new notion of computational indistinguishability: termination-insensitive computational indistinguishability (tic-indistinguishability). Tic-indistinguishability models indistinguishability with respect to distinguishers that cannot distinguish between termination and non-termination.
We sketch how the new notion allows to get computational soundness results of symbolic models for equivalence-based security properties (such as anonymity) for processes that contain loops, solving an open problem.
Abstract: Multiple notions of context-dependent computation, typically consisting in transformation of a homogeneous datastructure based on local rules applied uniformly to every node, are neatly analyzable in terms of comonads. Some examples include cellular automata execution, dataflow computation and attribute evaluation on trees. In this talk, I show that these examples also admit a finer analysis in terms of comodels of theories. This analysis explicitly dissects a notion of context into operations for observing contexts and equations they must satisfy. These operations make natural primitives for the corresponding languages of programming. But also natural primitives for these languages are combinators for generating/switching contexts, sending correctly constructed comodels to the unique homomorphism to the cofree comodel.
Needless to say, this is an attempt to dualize the tale of effectful notions of computation, monads, models of theories and effect constructing operations, incl. effect handlers à la Plotkin and Pretnar. Comodels were used by Power and Shkaravska's in an analysis of arrays.