- Dirk Draheim, "An Operational Semantics of Conditional Probabilities that Fully Adheres to Kolmogorov's Explication of Probability Theory"
Abstract: Classically, conditional probability is defined as P(A|B)=P(AB)/P(B). The definition is taken out of nothing, without reference to Kolmogorov's axioms and explication, i.e., it is not said which experiment P(_|B) stands for. Consequentially, the notion of conditional probability is not reinforced by an appropriate instance of the law of large numbers. We show that the gap can be filled. We construct a concrete P(_|B)-experiment that is about observing the Goodman-Nguyen-van Fraassen conditional event [A|B], i.e., the event of succeeding in A whenever B occurs for the first time in a series of repeated experiments. It is known that the probability of a conditional event P([A|B]) equals P(AB)/P(B). As opposed to the classical definition of P(A|B) the equation P([A|B])=P(AB)/P(B) is a result instead of a postulate! A probability P([A|B]) is directly understandable in terms of the Kolmogorov axioms and, similarly, an event [A|B] has an operational semantics that is directly justified by Kolmogorov's original explication of probability. We step beyond that. The observation of conditional events can be repeated itself. On basis of this, we achieve a strong law of large numbers for conditional events [A|B] that eventually reinforces the classic definition of conditional probability.
Link
- José Manuel Rodriguez Caballero, "Formal verification of theorems about Hilbert spaces in Isabelle/HOL"
Abstract: Unruh's quantum relational Hoare logic is a logical framework for verification of cryptographic protocols involving quantum phenomena. The mathematical background of this framework is the theory of Hilbert spaces. This talk is about my progress in formalizing the theory of Hilbert spaces in the proof assistant Isabelle/HOL.
Link
- Härmel Nestra, "Laws of Monadic Error Handling"
Abstract: One of the numerous applications of monads in functional programming is error handling. This work proposes several new axiomatics for equational reasoning about monadic computations with error handling and studies their relationships with each other and with axiomatics considered earlier. The primary intended application area is deterministic top-down parsing.
Proceedings of ICTAC 2019, LNCS (to appear)
- Behzad Abdolmaleki, "A Framework for UC-Secure Commitments from Publicly Computable Smooth Projective Hashing"\\ Abstract: Hash proof systems or smooth projective hash functions (SPHFs) have been proposed by Cramer and Shoup (Eurocrypt'02) and can be seen as special type of zero-knowledge proof system for a language. While initially used to build efficient chosen-ciphertext secure public-key encryption, they found numerous applications in several other contexts. In this paper, we revisit the notion of SPHFs and introduce a new feature (a third mode of hashing) that allows to compute the hash value of an SPHF without having access to neither the witness nor the hashing key, but some additional auxiliary information.We call this new type publicly computable SPHFs (PC-SPHFs) and present a formal framework along with concrete instantiations from a large class of SPHFs.
We then show that this new tool generically leads to commitment schemes that are secure against adaptive adversaries, assuming erasures in the Universal Composability (UC) framework, yielding the rst UC secure commitments build from a single SPHF instance. Instantiating our PC-SPHF with an SPHF for labeled Cramer-Shoup encryption gives the currently most efficient non-interactive UC-secure commitment. Finally, we also discuss additional applications to information retrieval based on anonymous credentials being UC secure against adaptive adversaries.
Joint work with: Hamidreza Khoshakhlagh, Daniel Slamanig
Accepted to IMA Cryptography and Coding 2019
- Martins Kokainis, "Quadratic speedup for finding marked vertices by quantum walks"
Abstract: A quantum walk algorithm can detect the presence of a marked vertex on a graph quadratically faster than the corresponding random walk algorithm (Szegedy, FOCS 2004). However, quantum algorithms that actually find a marked element quadratically faster than a classical random walk were only known for the special case when the marked set consists of just a single vertex, or in the case of some specific graphs. We present a new quantum algorithm for finding a marked vertex in any graph, with any set of marked vertices, that is (up to a log factor) quadratically faster than the corresponding classical random walk.
Joint work with: Andris Ambainis, András Gilyén, Stacey Jeffery
Link
- Helger Lipmaa, "Zk-SNARKs: Foundations and Applications"
Abstract: A ZK-SNARK (or Succinct Non-interactive Zero-Knowledge ARguments of Knowledge) enables one participant (a prover) to convince another participant (a verifier) in the correctness of some statement without leaking any side information. It is also required that a zk-SNARK satisfies quite strong efficiency properties; in particular, the prover should only send a single succinct message to the verifier and the amount of verifier's computation should not depend on the statement's complexity. While the constructions of ZK-SNARKs are quite complicated, recent advances have made them efficient enough so that they are used in applications like the zcash cryptocurrency where one hides the contents of each transaction but then accompanies a transaction with a zk-SNARK argument of transaction correctness. Perhaps unsurprisingly, zk-SNARKs were listed as one of the ten technological breakthroughs of 2018 by the MIT Technology Review. In this talk, we will explain what a zk-SNARK is, describe some applications, and explain how they are constructed and why they might be secure.
- Abuzer Yakaryilmaz, "Quantum programming with Qiskit"
Abstract: I will explain how to write basic quantum programs by using Qiskit library. I will provide a few interesting examples. I will use a material that we have been using to organize three-day long workshops.
Link
- Lilia Safina, "The Quantum Version Of Classification Decision Tree Constructing Algorithms"
Abstract: We consider decision tree as a model for the classification problem from machine learning. We focus on complexity of decision tree constructing algorithms as C5.0, CART. In classical case the decision tree is constructed in {$O(hd(NM+N \log N))$} running time, where {$M$} is a number of classes, {$N$} is the size of a training data set, {$d$} is a number of attributes of each element, {$h$} is a tree height. Firstly, we improve the classical version, the running time of the new version is {$O(h\cdot d\cdot N\log N)$}. Secondly, we suggest a quantum version of this algorithm, which uses the D{\"u}rr-H{\o}yer minimum search quantum algorithm as subroutine that is based on Grover's algorithm. The running time of the quantum algorithm is {$O\big(h\cdot \sqrt{d}\log d \cdot N \log N\big)$} that is better than complexity of the classical algorithm.
Joint work with: Ilnaz Mannapov, Kamil Khadiev
Link
The work is based on the paper that was presented at YSIP 2019
- Janno Siim, "UC-Secure CRS Generation for SNARKs"
Abstract: Zero-knowledge SNARKs (zk-SNARKs) have recently found various applications in verifiable computation and blockchain applications (Zerocash), but unfortunately they rely on a common reference string (CRS) that has to be generated by a trusted party. A standard suggestion, pursued by Ben Sasson et al. [IEEE S&P, 2015], is to generate CRS via a multi-party protocol. We enhance their CRS-generation protocol to achieve UC-security. This allows to safely compose the CRS-generation protocol with the zk-SNARK in a black-box manner with the insurance that the security of the zk-SNARK is not influenced. Differently from the previous work, the new CRS-generation protocol also avoids the random oracle model which is typically not required by zk-SNARKs themselves. As a case study, we apply the protocol to the state-of-the-art zk-SNARK by Groth [EUROCRYPT, 2016].
Joint work with: Behzad Abdolmaleki, Karim Baghery, Helger Lipmaa, Michal Zajac
Link
Africacrypt 2019
- Pawel Sobocinski, "Tutorial on String Diagrams and Compositionality"
Abstract: I will give a tutorial/introduction talk on my area and related topics.
- Karim Baghery, "On the Efficiency of Privacy-Preserving Smart Contract Systems"
Abstract: Along with blockchain technology, smart contracts have found intense interest in lots of practical applications. A smart contract is a mechanism involving digital assets and some parties, where the parties deposit assets into the contract and the contract redistributes the assets among the parties based on provisions of the smart contract and inputs of the parties. Recently, several smart contract systems are constructed that use zk-SNARKs to provide privacy-preserving payments and interconnections in the contracts (e.g. Hawk [IEEE S&P, 2016] and Gyges [ACM CCS, 2016]). Efficiency of such systems severely are dominated by efficiency of the underlying UC-secure zk-SNARK that is achieved using COCO framework [Kosba et al., 2015] applied on a non-UC-secure zk-SNARK. In this research, we show that recent progresses on zk-SNARKs, allow one to simplify the structure and also improve the efficiency of both systems with a UC-secure zk-SNARK that has simpler construction and better efficiency in comparison with the currently used ones. To this end, we first show that given a NIZK argument which guarantees non-black-box simulation (knowledge) soundness, one can construct a UC-secure NIZK that has simpler construction and better efficiency than the ones that currently are used in Hawk and Gyges. We believe, new technique can be of independent interest.
Link
AFRICACRYPT 2019
- Shahla Atapoor, "Simulation Extractability in Groth's zk-SNARK"
Abstract: A Simulation Extractable (SE) zk-SNARK enables a prover to prove that she knows a witness for an instance in a way that the proof: (1) is succinct and can be verified very efficiently; (2) does not leak information about the witness; (3) is simulation-extractable -an adversary cannot come out with a new valid proof unless it knows a witness, even if it has already seen arbitrary number of simulated proofs. Non-malleable succinct proofs and very efficient verification make SE zk-SNARKs an elegant tool in various privacy-preserving applications such as cryptocurrencies, smart contracts and etc. In Eurocrypt 2016, Groth proposed the most efficient pairing-based zk-SNARK in the CRS model, but its proof is vulnerable to the malleability attacks. In this research, we show that one can efficiently achieve simulation extractability in Groth's zk-SNARK by some changes in the underlying language using a folklore OR construction. Analysis and implementations show that in practical cases overload has minimal effects on the efficiency of original scheme which currently is the most efficient zk-SNARK. In new construction, proof size is extended with one element from G1, one element from G2, plus a bit string that totally is less than 256 bytes for 128-bit security. Its verification is dominated with 4 pairings which is the most efficient verification among current SE zk-SNARKs.
Joint work with: Karim Baghery
Link
ESORICS Workshop on Cryptocurrencies and Blockchain Technology - CBT'19
- Pille Pullonen, "Privacy-Enhanced Business Process Model and Notation"
Abstract: Privacy-enhancing technologies play an important role in preventing the disclosure of private data as information is transmitted and processed. Although business process model and notation (BPMN) is well suited for expressing stakeholder collaboration and business processes support by technical solutions, little is done to depict and analyze the flow of private information and its technical safeguards as it is disclosed to process participants. This gap motivates the development of privacy-enhanced BPMN (PE-BPMN) -- a BPMN language extension for capturing PET-related activities in order to study the flow of private information and ease the communication of privacy concerns and requirements among stakeholders. We demonstrate its feasibility in a mobile app scenario and present techniques to analyze information disclosures identified by models enriched with PE-BPMN.
Joint work with: Jake Tom, Raimundas Matulevicius, Dan Bogdanov, Aivo Toots
Link 1 and Link 2
Conference version published in BPM 2019, journal version in Software and Systems Modeling: December 2019
- Andris Ambainis, "Recent developments in quantum algorithms"
Abstract: I will survey recent developments in quantum algorithms, including research at the Centre for Quantum Computer Science, University of Latvia. The topics will include:
- algorithms for near term quantum computers, such as quantum approximate optimization (QAOA);
- quantum speedups and quantum lower bounds for classical algorithms based on dynamic programming;
- possibility of quantum speedups for problems that have classical lower bounds under one of fine-grained complexity conjectures (such as Strong Exponential Time Hypothesis or SETH);
- quantum search algorithms based on quantum walks.
- Peeter Laud, "Information flow analysis for BPMN processes"
Abstract: We present a precise information-flow analysis for communicating processes, expressed using Business Processes Model and Notation (BPMN). We start by giving a semantics for the communication, which avoids the non-deterministic pair-ups between sending and receiving events. We will then present a transformation from the processes to a data dependency graph with replications; we show what kinds of nodes this graph must have in order to represent the control flow of the original processes. The information flow analysis consists of simplifying the obtained graph; we will describe the most significant simplifications.
- Alisa Pankova, "Taming epsilon of differential privacy"
Abstract: Differential privacy is a nice definition that quantifies privacy of an individual record x in a database. Formally, it tells that, for any possible observed output y, it should be hard to distinguish whether x was in the database or not. The 'hardness' of distinguishing is characterized by a parameter {$\varepsilon$} that is different from standard cryptographic notions like attacker's advantage, and the 'goodness' of {$\varepsilon$} is relative, depending on the actual data and its distribution. In this talk, we discuss relations between{$\varepsilon$} and the attacker's guessing advantage, providing a way with coming up with an optimal {$\varepsilon$} value depending on the privacy requirements.
Joint work with: Peeter Laud
- Hendrik Maarand, "Reordering Derivatives of Trace Closures of Regular Languages"
Abstract: We provide syntactic derivative-like operations, defined by recursion on regular expressions, in the styles of both Brzozowski and Antimirov, for trace closures of regular languages. Just as the Brzozowski and Antimirov derivative operations for regular languages, these syntactic reordering derivative operations yield deterministic and nondeterministic automata respectively. But trace closures of regular languages are in general not regular, hence these automata cannot generally be finite. Still, as we show, for star-connected expressions, the Antimirov and Brzozowski automata, suitably quotiented, are finite. We also define a refined version of the Antimirov reordering derivative operation where parts-of-derivatives (states of the automaton) are nonempty lists of regular expressions rather than single regular expressions. We define the uniform scattering rank of a language and show that, for a regular expression whose language has finite uniform scattering rank, the truncation of the (generally infinite) refined Antimirov automaton, obtained by removing long states, is finite without any quotienting, but still accepts the trace closure. We also show that star-connected languages have finite uniform scattering rank.
Joint work with: Tarmo Uustalu
Link
CONCUR 2019
- Kamil Khadiev, "Quantum Algorithms for String Problems"
Abstract: We study algorithms for solving several problems on strings. The first one is the Most Frequently String Search Problem. The problem is the following. Assume that we have a sequence of {$n$} strings of length {$k$}. The problem is finding the string that occurs in the sequence most often. We propose a quantum algorithm that has a query complexity {$\tilde{O}(n \sqrt{k})$}. This algorithm shows speed-up comparing with the deterministic algorithm that requires {$\Omega(nk)$} queries.
The second one is searching intersection of two sequences of strings. All strings have the same length {$k$}. The size of the first set is {$n$}, and the size of the second set is {$m$}. We propose a quantum algorithm that has a query complexity {$\tilde{O}((n+m) \sqrt{k})$}. This algorithm shows speed-up comparing with the deterministic algorithm that requires {$\Omega((n+m)k)$} queries.
The third problem is sorting of {$n$} strings of length {$k$}. On the one hand, it is known that quantum algorithms cannot sort objects asymptotically faster than classical ones. On the other hand, we focus on sorting strings that are not arbitrary objects. We propose a quantum algorithm that has a query complexity {$O(n (\log n)^2 \sqrt{k})$}. This algorithm shows speed-up comparing with the deterministic algorithm (radix sort) that requires {$\Omega((n+d)k)$} queries, where {$d$} is a size of the alphabet.
The fourth problem is constructing a string (text) from another set of strings (dictionary). The size of the text is {$n$}, a number of strings in the dictionary is {$m$} and the length of each dictionary string is at most {$k$}. There are two kinds of problem. In the first one, we allow using strings from the dictionary several times, in the second one each dictionary string should be used at most ones. We suggest quantum algorithms for both kinds of the problem. An algorithm for the first kind works in {$O(\sqrt{m}n(\log n)^2)$} running time; and for the second kind, an algorithm works in {$O(1.728^{n}(n)^2)$}.
Joint work with: Artem Ilikaev, Vladislav Remidovsky
The talk is extended version of the work that was accepted in TPNC2019
- Nikolajs Nahimovs, "Lackadaisical quantum walks with multiple marked vertices"
Abstract: The concept of lackadaisical quantum walk -- quantum walk with self loops -- was first introduced for discrete-time quantum walk on one-dimensional line. Later it was successfully applied to improve the running time of the spacial search on two-dimensional grid.
We study search by lackadaisical quantum walk on the two-dimensional grid with multiple marked vertices. First, we show that the lackadaisical quantum walk, similarly to the regular (non-lackadaisical) quantum walk, has exceptional configuration, i.e. placements of marked vertices for which the walk has no speed-up over the classical exhaustive search. Next, we demonstrate that the weight of the self-loop suggested in the previous papers is not optimal for multiple marked vertices. And, last, we show how to adjust the weight of the self-loop to overcome the aforementioned problem.
Link
Paper
- Vitaly Skachek, "Batch and PIR Codes and Their Connections to Locally Repairable Codes"
Abstract: In this survey talk, we discuss two related families of codes: batch codes and codes for private information retrieval. These two families can be viewed as natural generalizations of locally repairable codes, which were extensively studied in the context of coding for fault tolerance in distributed data storage systems. Bounds on the parameters of the codes, as well as basic constructions, are presented. Connections between different code families are discussed.
This talk is inspired by collaborations with Helger Lipmaa, Sushanta Paudyal, Ago-Erik Riet, Eldho K. Thomas, Hui Zhang, and Jens Zumbraegel
Link
"Batch and PIR codes and their connections to locally repairable codes." Network Coding and Subspace Designs. Springer, Cham, 2018. 427-442.
- Francico Javier Gil Vidal, "Input Redundancy for Parameterized Quantum Circuits"
Abstract: This talk deals with a special type of parameterized quantum circuits, the so-called quantum neural networks or QNN's, which are trained to estimate a given function, specifically the type of circuits proposed by Mitarai et al. in their seminal 2018 paper (Mitarai, Negoro, Kitagawa & Fujii 2018. Quantum Circuit Learning. arXiv:1803.00745.). Interest in that paper has been considerable, since it promises to, at least partially, bridge the gap between the possibilities of currently hard-to-implement quantum algorithms and the actual capabilities of near-term quantum processors. A quantum circuit driven by the framework therein proposed learns a given task by tuning parameters implemented on it. To ease the difficulties attending the actual implementation of large-scale quantum circuits, Mitarai et al. resort to hybridization of a low-depth quantum circuit and a classical computer for machine learning, making the task more accessible to near-term quantum devices.The input is encoded into amplitudes of states of qubits; a fuller explanation of what this means is given in the talk.
The no-cloning principle of quantum mechanics suggests that there is an advantage in redundantly encoding the input value several times. We follow this suggestion, and prove lower bounds on the number of redundant copies for two types of input encoding. From that, we draw conclusions for the architecture design of QNNs.
Joint work with: Dirk Oliver Jim Theis
- Silvio Capobianco, "Boltzmann samplers: a tutorial"
Abstract: A combinatorial class is a set C with a size function taking values in the nonnegative integers such that, for every n, the subset C[n] of elements of size n is finite. A combinatorial class can be described by its generating function, which is a formal power series in the complex plane.
A Boltzmann model for a combinatorial class C is a probability distribution on the objects of C which is uniform on each subset C[n]. Such distributions can be "tuned" by exploiting suitable properties of the generating function. A Boltzmann sampler is a random generator with distribution following a Boltzmann model.
In this tutorial, we will initially discuss the basic of the theory of power series, which have a central role in analytic combinatorics. We will then introduce Boltzmann samplers and show how constructions on combinatorial classes yield constructions for their Boltzmann samplers. We will conclude with a discussion about applications of Boltzmann samplers in software testing.
- Oliver-Matis Lill, "Decentralized Bitcoin Scaling with Specialization"
Abstract: Bitcoin is a young cryptocurrency that has seen an explosive growth of popularity in recent years. If the trend continues, then due to the design of the Bitcoin network it will end up facing serious scalability issues. With the current node behavior, allowing large transaction rates would lead to centralization. Restricting transaction rates however might kill off Bitcoins chance of achieving its potential as a general purpose currency. In this paper we present a method to combat centralization in the case of high transaction rates. Specifically we propose to move the task of transaction validation to specialized validator nodes and further present a system that allows them to divide up the work while ensuring that the blockchain gets thoroughly validated. We also propose a set of protocols to allow the new miners and validators to cooperate for block mining and for ensuring the trustworthiness of the blockchain. Finally, we study practical aspects and possible threats to the presented system, and propose countermeasures.
Link
- Tähvend Uustalu, "Constructing bipartite graphs without short cycles"
Abstract: In this talk, we present an experimental approach for constructing bipartite graphs without short cycles. This approach is based on a variation of simulated annealing algorithm. The constructed graphs can be interpreted as Tanner graphs of LDPC codes, thus yielding constructions of (non-binary) LDPC codes possessing low error floor.
- Jevgenijs Vihrovs, "Cuts, Flows and Quantum Walks"
Abstract: In this talk we discuss how the eigenstates of the quantum walk with Grover's diffusion coin relate to the cycle and cut spaces of the graph. More specifically, it has been known that eigenstates with eigenvalue –1 span the cycle space of the graph. Here we show some connections to the theory of electrical networks. For example, we prove that measuring a uniformly random quantum eigenstate with eigenvalue –1 in the standard edge basis is equivalent to sampling edges in proportion to their effective electrical resistances in the graph.
Joint work with: Anupam Prakash
- Aliia Khadieva, "Quantum minicomplexity"
Abstract: We investigate the complexity classes for quantum automata. We explore different models such as quantum finite automata, nondeterministic quantum finite automata of exponential, polynomial size. We show relations of complexity classes for quantum and classical models, giving concrete languages as witnesses that distinct different classes. We call this topic quantum minicomplexity, inspired by a work "Minicomplexity" of Christos A. Kapoutsis.
Joint work with: Abuzer Yakaryilmaz, Kamil Khadiev
- Niccolò Veltri, "Unguarded Iteration for Reversible Computation in the Delay Monad"
Abstract: Reversible computation studies computations which exhibit both forward and backward determinism. Among others, it has been studied for half a century for its applications in low-power computing, and forms the basis for quantum computing.
Though certified program equivalence is useful for a number of applications (e.g., certified compilation and optimization), little work on this topic has been carried out for reversible programming languages. As a notable exception, Carette and Sabry have studied the equivalences of the finitary fragment of Πo, a reversible combinator calculus, yielding a two-level calculus of type isomorphisms and equivalences between them. In this paper, we extend the two-level calculus of finitary Πo to one for full Πo (i.e., with both recursive types and iteration by means of a trace combinator) using the delay monad, which can be regarded as a “computability-aware” analogue of the usual maybe monad for partiality. This yields a calculus of iterative (and possibly non-terminating) reversible programs acting on user-defined dynamic data structures together with a calculus of certified program equivalences between these programs.
Joint work with: Robin Kaarsgaard
Agda formalization
This talk is based on a paper accepted for publication at the 13th International Conference on Mathematics of Program Construction (MPC 2019)
- Nikita Larka, "Quantum algorithms for computational geometry problems"
Abstract: One of the important problems in theoretical computer science is 3SUM problem. One can formulate 3SUM problem as follows: given a set {$S$} of {$n$} integers, are there {$a, b, c \in S$}, such that {$a + b + c = 0$}. Existence of an algorithm that solves this problem in time {$O(n^{2 - \epsilon})$} is open problem in computer science. 3SUM problem can be reduced to many geometrical problems and so, there is no algorithm to solve those problems in {$O(n^{2 - \epsilon})$}.
In this paper we study quantum algorithms for geometrical 3SUM-HARD problems, those are the problems that are as hard as 3SUM problem. An example of this kind of problem is POINT-ON-3-LINES problem. In this problem we are given a set of lines and we are asked to find a point that lies on at least {$3$} of given lines. We present a quantum algorithm that solves this problem in time {$O(n^{1 + o(1)})$}. The techniques we use combine amplitude amplification with geometrical ideas. We show that the same ideas can give {$O(n^{1 + o(1)})$} time algorithm for many 3SUM-HARD class geometrical problems.
Joint work with: Andris Ambainis
- Alexander Belov, "Some Results in Property Testing"
Abstract: The field of property testing deals with the following question. Given an object, detect whether it satisfies some property or is far from doing so. Usually, the object is modeled as a bit-string, and the distance is (relative) Hamming distance. The goal is to develop an algorithm whose complexity is very small: much smaller than the size of the object.
In this talk, I will survey some of the classical and recent results in property testing, covering both my own contribution and work by other people. The focus will be on properties of functions: monotonicity and convexity.
Some of my results are joint work with Eric Blais from the University of Waterloo.
- Hellis Tamm, "Quotients and Atoms of Reversible Languages"
Abstract: We consider several reversible finite automaton models which have been introduced over decades, and study some properties of their languages. In particular, we look at the question whether the quotients and atoms of a specific class of reversible languages also belong to that class or not. We consider bideterministic automata, reversible deterministic finite automata (REV-DFAs), reversible multiple-entry DFAs (REV-MeDFAs), and several variants of reversible nondeterministic finite automata (REV-NFAs). It is known that the class of REV-DFA languages is strictly included in the class of REV-MeDFA languages. We show that the classes of complete REV-DFA languages and complete REV-MeDFA languages are the same. We also show that differently from the general case of a REV-DFA language, the minimal DFA of a complete REV-DFA language is a complete REV-DFA. We also show that atoms of any regular language are accepted by REV-NFAs with a single initial and a single final state.
Accepted to RPLA 2019
- Dominique Unruh, "Towards verified quantum crypto"
Abstract: We are currently working towards the formal verification (using theorem provers) of the security of quantum cryptographic protocols. In this talk, I will describe the context of that research, our progress, and challenges faced.
- Tarmo Uustalu, "Resumption Monads for Shared-Memory Concurrency"
Abstract: I will describe a denotational approach to shared-memory concurrency where interaction of threads through shared memory is treated as an effect modelled with monads of resumptions. 'Resumption' is a general term for datastructures for describing computations in terms of sequences of small steps. The resumption monads I consider are concurrent monads in the sense recently proposed by Jaskelioff and Rivas: a monad structure accounting for sequential composition agrees in a certain way with a lax monoidal functor structure describing parallel composition.
This talk is based on an extended abstract distributed at RADICAL 2019