Ettekanded / Talks

Martin Aher: You're in the wrong: a violation-based challenge to standard semantics for modals

Slides from the talk [pdf]

Abstract: I will discuss several well-known puzzles in the philosophy and linguistics literature surrounding deontic modals such as permission, obligation and prohibition. I propose to solve these puzzles by introducing a novel semantic treatment of deontic modals based on violations and alternatives. The talk focuses on the free choice puzzle and deontic conflicts but I will also discuss the broad issue of monotonicity puzzles, and some puzzles arising from the interaction between conditionals and modals.

An interdisciplinary study of WTO legal texts revealed that judges explicitly refer to violations of rules. To capture this in the semantics, I adopt an Andersonian approach which analyzes deontic modals as implications to violations. I modify Anderson's original account in the tradition of alternative-based semantics by adding quantification over alternatives. This allows us to account for the intuitive difference between the behaviour of implications and deontic modals under negation.

However, unlike in the alternative-based semantics of Aloni, I suggest that obligation, similarly to permission, ought to also apply to every alternative. Such a treatment of deontic modals is motivated by the idea that deontic modality rejects ignorance readings or inquisitive readings where it is not known which information holds. Intuitively, the authors of a rule establish what is permitted/prohibited/obligatory, and this leaves no room for ignorance. So, I propose that deontic modals always quantify universally over alternatives.

The deontic modals are realized within the framework of radical inquisitive semantics developed by Groenendijk, Roelofsen and Sano because it provides several advantages. For example, the standard treatment of conditional sentences in the literature is based on a semantics for modal expressions. The radical framework also provides a treatment of conditional sentences which attains similar predictions to the widely accepted Kratzer account of conditionals and, most importantly, avoids the puzzles of material implication.

The semantics makes intuitive predictions concerning the free choice puzzle. As the deontic modals are Andersonian, the standard behaviour of disjunction in the antecedent of an implication accounts for the intuition that permission is granted to both disjuncts. Furthermore, the modification to add universal quantification over alternatives to Andersonian violation-semantics provides a semantic solution to the behaviour of free choice examples under negation, which has proven challenging for most accounts in the literature.

Introducing violations directly into the semantics allows us to account for deontic conflicts, i.e., situations where one cannot avoid violating all rules. For example, when there is a conflict of obligations, and one cannot avoid violating at least one of the obligations, a semantics ought to represent this situation as a choice between unfortunate consequences. I solve the puzzle by introducing several atoms for violations.

The proposed deontic operators are not upward monotonic, so counter-intuitive predictions of Ross's puzzle do not go through. This also applies to the Dr. Procrastinate puzzle where the combination of introducing multiple violations and non-monotonicity of modals provides an intuitive prediction concerning the situation.At the end of the talk, I will discuss one of the consequences of adopting a radical framework - the introduction of gaps, i.e., information which both supports and rejects a proposition. Illustrated by the conditional oughts puzzle, I argue that further research needs to focus on these gaps to overcome inherent difficulties in the semantics and to solve some remaining puzzles.

Abel Armas Cervantes: Behavioral comparison of process models based on canonically reduced event structures

Slides from the talk [pptx]

Abstract: This presentation addresses the problem of diagnosing behavioral differences between pairs of business process models. The proposed solution is based on a translation from process models to Asymmetric Event Structures (AES). We propose a technique to reduce event duplication in an AES while preserving canonicity. Additionally, we present a notion of unfolding that captures all possible causes of each event in a cycle. From there we derive an AES where repeated events are distinguished from non-repeated ones and that allows us to diagnose differences in terms of repetition and causal relations in one model but not in the other.

Juhan Ernits: Pushing the limits of code duels: teaching and learning of AI algorithms

Abstract: Symbolic execution has recently been applied for online teaching and learning of programming in the Pex4Fun project. In the current work we extend the Pex based code duels framework to teaching and learning of algorithms involving nontrivial data structures. In order to control various parameters of the environment and Pex and perform empirical analysis, we implemented an environment similar to Pex4Fun. While increasing the time and character count limits over those of Pex4Fun for the algorithms teaching system was straight forward, succeeding in generating various data structures required fine tuning of a number of parameters. We present the empirical results of tuning Pex for teaching and learning of several search algorithms, arc consistency algorithm AC-3, and DPLL.

Wolfgang Jeltsch: Categorical semantics for functional reactive programming with temporal recursion and corecursion

Slides from the talk [pdf]

Abstract: Functional reactive programming (FRP) makes it possible to express temporal aspects of computations in a declarative way. Recently, we developed two kinds of categorical models of FRP: abstract process categories (APCs) and concrete process categories (CPCs). Furthermore, we showed that APCs generalize CPCs. In this talk, we extend APCs with additional structure. This structure models recursion and corecursion operators that are related to time. We argue that the resulting categorical models generalize those CPCs that impose an additional constraint on time scales. This constraint boils down to ruling out ω-supertasks, which are closely related to Zeno's paradox of Achilles and the tortoise.

This work was presented at MSFP 2014.

Toomas Krips: A hybrid model of fixed and floating point numbers in secure multiparty computations

Abstract: We developed fixed-point numbers for the secure multiparty computation platform Sharemind. We also used Chebyshev polynomials and Taylor polynomials to implement square root, inverse, the exponential function and the error functions on fixed-point numbers and on a hybrid version of fixed-point numbers and floating-point numbers.

Risto Laanoja: Efficient quantum-immune keyless signatures with identity

Slides from the talk [pdf]

Abstract: We show how to extend hash-tree based data signatures to server-assisted personal digital signature schemes. The new signature scheme does not use trapdoor functions and is based solely on cryptographic hash functions and is thereby, considering the current state of knowledge, resistant to quantum computational attacks. In the new scheme, we combine hash-tree data signature (time-stamping) solutions with hash sequence authentication mechanisms. We show how to implement such a scheme in practice.

This is joint work with Ahto Buldas and Ahto Truu.

Peeter Laud: Privacy-preserving processing of regular languages

Slides from the talk [pdf]

Abstract: Regular languages, represented through finite automata, have many applications with various security and privacy requirements. In this talk, we will describe privacy-preserving protocols for certain tasks working with deterministic finite automata, namely the word problem, and the minimization. For the latter problem, we employ oblivious extended permutations, a primitive introduced recently for private function evaluation. We will perform a deeper study of this primitive, and introduce a simpler, more generic, and possibly more efficient version. We present a range of privacy-preserving algorithms for constructing and applying extended permutations, providing the foundations for integrating this primitive into secure computation platforms.

Fabrizio Maria Maggi: Predictive monitoring of business processes

Slides from the talk [pdf]

Abstract: Modern information systems that support complex business processes generally maintain significant amounts of process execution data, particularly records of events corresponding to the execution of activities (event logs). In this talk, I am presenting an approach to analyze such event logs in order to predictively monitor business goals during business process execution. At any point during an execution of a process, the user can define business goals in the form of linear temporal logic rules. When an activity is being executed, the framework identifies input data values that are more (or less) likely to lead to the achievement of each business goal. Unlike reactive compliance monitoring approaches that detect violations only after they have occurred, our predictive monitoring approach provides early advice so that users can steer ongoing process executions towards the achievement of business goals. In other words, violations are predicted (and potentially prevented) rather than merely detected.

Keiko Nakata: A recursive type system with type abbreviations and abstract types

Slides from the talk [pdf]

Abstract: Although theories of equivalence or subtyping for recursive types have been extensively investigated, sophisticated interaction between recursive types and abstract types has gained little attention. The key idea behind type theories for recursive types is to use syntactic contractiveness, meaning every μ-bound variable occurs only under a type constructor such as → or ×. This syntactic contractiveness guarantees the existence of the unique solution of recursive equations and thus has been considered necessary for designing a sound theory for recursive types. However, in an advanced type system, such as OCaml, with recursive types, type parameters, and abstract types, we cannot easily define the syntactic contractiveness of types. In this paper, we investigate a sound type system for recursive types, type parameters, and abstract types. In particular, we develop a new semantic notion of contractiveness for types and signatures using mixed induction and coinduction, and show that our type system is sound with respect to the standard call-by-value operational semantics, which eliminates signature sealings. Moreover we show that while non-contractive types in signatures lead to unsoundness of the type system, they may be allowed in modules. We have also formalized the whole system and its type soundness proof in Coq.

This is joint work with Hyeonseung Im and Sungwoo Park, was presented at ICALP 2013.

Härmel Nestra: Software for instructors preparing algorithm visualization examples

Slides from the talk [pdf]

Abstract: We demonstrate our software, written in OCaml, which has been developed for easy preparation of examples about how classic algorithms work. The intended users are the bachelor level Algorithms and Data Structures course instructors. Using this software, the instructor can automatically generate slide shows that act the behaviour of chosen algorithms. Contrasting to typical applications that trace executions of algorithm code line-by-line, the slide shows generated by this software are designed to support basic understanding of the idea of the algorithm, for what reason programming details are intensionally ignored. The slides should help the weaker students who have difficulties with understanding the abstract descriptions of algorithms in textbooks to get the general idea.

Alisa Pankova: Verifiable computation in multiparty protocols with honest majority

Slides from the talk [pdf]

Abstract: A lot of cryptographic protocols have been proposed for semi-honest model. In general, they are much more efficient than those proposed for the malicious model. In this paper, we propose a method that allows to detect the parties that have violated the protocol rules after the computation has ended, thus making the protocol secure against covert attacks. This approach can be useful in the settings where for any party it is fatal to be accused in violating protocol rules. In this way, up to the verification, all the computation can be performed in semi-honest model, which makes it very efficient in practice. The verification is statistical zero-knowledge, and it is based on linear probabilistically checkable proofs (PCP) for verifiable computation. Each malicious party is detected with probability (1 - e) for a negligible e that is defined by the failure of the corresponding linear PCP. The initial protocol has to be executed only once, and the verification requires in total 5 additional rounds in the end. If some parties act dishonestly, in the worst case they may force the protocol to substitute each round with 2 rounds, due to the transmission functionality that prevents the protocol from stopping. The verification also ensures that all the parties have sampled all the randomness from an appropriate distribution. Its efficiency does not depend on whether the inputs of the parties have been shared, or each party uses its own private input.

This is joint work with Peeter Laud.

Martin Pettai: Automatic proofs of privacy of secure multi-party computation protocols against active adversaries

Slides from the talk [pdf]

Abstract: We describe an automatic analysis to check secure multiparty computation protocols against privacy leaks. The analysis is sound - a protocol that is deemed private does not leak anything about its private inputs, even if active attacks are performed against it. Privacy against active adversaries is an essential ingredient in constructions aiming to provide security (privacy + correctness) in adversarial models of intermediate (between passive and active) strength. Using our analysis we are able to show that the protocols used by the Sharemind secure multiparty computation platform are actively private.

This is joint work with Peeter Laud.

Pille Pullonen: From input-private to universally composable secure multiparty computation

Slides from the talk [pdf]

Abstract: Secure multiparty computation systems are commonly built form a small set of primitive components. If the initial blocks are composable then we can infer the security properties of the composed system from the properties of the initial components. The standard notions of universally composable security can be overly restrictive in secure multiparty computation context and can lead to protocols with sub-optimal efficiency as additional steps are required to make the functionality secure. As a countermeasure, we introduce a notion of privacy that is satisfied by simpler protocols and is preserved by composition. We also fix a passive security model and show how to convert a black-box private protocol into a black-box universally composable protocol in the passive model. Therefore, we obtain a possibility to compose secure protocols out of efficient private protocols and a secure universally composable finishing step.

This is joint work with Dan Bogdanov, Peeter Laud, Sven Laur, to be presented at CSF '14.

Sander Siim: Secure multiparty computation protocols from a high-level programming language

Slides from the talk [pdf]

Abstract: Secure multiparty computation (SMC) enables privacy-preserving computations on data originating from a number of parties. In today's digital world, data privacy is increasingly more difficult to provide. With SMC methods like secret sharing and Yao's garbled circuits, it is possible to build privacy-preserving computational protocols that do not leak confidential input to other parties. The additive secret sharing scheme is very efficient for algebraic ring operations on fixed bit-length data types, but protocols that require robust bit-level manipulation are difficult to build. Yao's garbled circuits approach however works on arbitrary bit-length data and allows evaluation of any Boolean function.

Combining the two methods, we present a hybrid protocol, which provides a general method to build arbitrary secure computations on bitwise secret-shared data. We are able to generate circuits for the protocol easily by using two state-of-the-art C to circuit compilers designed for SMC applications. We briefly describe both and compare the two in terms of functionality and efficiency. We also discuss the security of our hybrid protocol and describe our prototype implementation on the Sharemind privacy-preserving computational platform.

Tarmo Uustalu: Bi-intuitionistic logics and modal logic

Abstract: I will review some basic facts about two incredibly cool logics - Rauszer's bi-intuitionistic (propositional) logic and Bellin's alternative version. Both symmetrize intuitionistic propositional logic, but in different ways, and both resulting logical systems are full of surprises. I will focus on their Kripke semantics and translations to modal logics.

Niccolō Veltri: The delay monad in general categories

Abstract: tba

Liina Kamm
Peeter Laud
Helger Lipmaa
Tarmo Uustalu
Varmo Vene
Viimane uuendus 24.5.2014