VSL 2014: VIENNA SUMMER OF LOGIC 2014
DCM ON SUNDAY, JULY 13TH, 2014

View: session overviewtalk overviewside by side with other conferences

09:15-10:15 Session 24A: Joint DCM / TermGraph Invited Talk (joint with TermGraph)
Location: FH, Seminarraum 325/2
09:15
Numeral Systems in the Lambda Calculus
SPEAKER: Ian Mackie

ABSTRACT. We investigate numeral systems in the λ-calculus; specifically
in the linear λ-calculus where copying and erasing are not
permitted. Our interest is in finding efficient (and where possible,
in constant time) representations for successor, predecessor,
addition, subtraction and test for zero.  We begin by recalling some
well-known systems, before going on to the linear case where we give
several systems with different properties. We conclude with a
characterisation of linear numeral systems.

10:15-10:45Coffee Break
10:45-11:45 Session 26T
Location: FH, Seminarraum 138B
10:45
A Simple Parallel Implementation of Interaction Nets in Haskell
SPEAKER: Wolfram Kahl

ABSTRACT. Due to their ``inherent parallelism'', interaction nets have since their introduction been considered as an attractive implementation mechanism for functional programming. We show that a simple highly-concurrent implementation in Haskell can achieve promising speed-ups on multiple cores.

11:15
Some observations for the parallel implementation of interaction nets
SPEAKER: Shinya Sato

ABSTRACT. There have been several studies about the parallel implementation of interaction nets. Here we look at the related question: when is an interaction net system suitable for parallel evaluation? Some systems are sequential, some have the potential to be highly parallel. This first investigation aims to throw some light on this topic, and perhaps help pave the way to wider use of this technology for parallel evaluation. In this short paper we focus on presenting experimental evidence in a number of small case studies.

12:00-13:00 Session 29C
Location: FH, Seminarraum 138B
12:00
Quantitative semantics for higher-order probabilistic and quantum computation
ABSTRACT.
Various models of Linear Logic have been defined in categories of
vector spaces (more generally modules) and linear functions. These
models provide semantics of quite expressive functional programming
languages, where programs using their inputs exactly once correspond
to linear functions and programs using their inputs an arbitrary
number of times (like recursive programs) correspond to power series.

Quantitative semantics are particularly suitable for interpreting
non-deterministic computations, such as probabilistic and quantum
algorithms. The addition between vectors expresses a kind of
superposition of atomic states and the scalars a quantitative
estimation of this superposition.

In this talk I will introduce to the main ideas of quantitative
semantics and I will present the most recent results achieved in the
framework of higher-order probabilistic and quantum computation.
13:00-14:30Lunch Break
14:30-16:00 Session 31R
Location: FH, Seminarraum 138B
14:30
Cellular Automata are Generic
SPEAKER: unknown

ABSTRACT. We show that any effective algorithm over any arbitrary domain can be simulated by a particular kind of dynamic cellular automaton

15:00
Quantum Circuits for the Unitary Permutation Problem
SPEAKER: unknown

ABSTRACT. We consider the Unitary Permutation problem which consists, given n unitary gates U_1,…,U_n and a permutation σ of {1,…,n}, in applying the unitary gates in the order specified by σ, i.e. in performing U_σ(n)…U_σ(1).

This problem has been introduced and investigated by Colnaghi et al. where two models of computations are considered. This first is the (standard) model of query complexity: the complexity measure is the number of calls to any of the unitary gates U_i in a quantum circuit which solves the problem. The second model provides quantum switches and treats unitary transformations as inputs of second order. In that case the complexity measure is the number of quantum switches. In this seminal paper it has been shown that the problem can be solved within n^2 calls in the query model and n(n-1)/2 quantum switches in the new model.

We refine these results by proving that nlog_2(n)+\Theta(n) quantum switches are necessary and sufficient to solve this problem, whereas n^2-2n+4 calls are sufficient to solve this problem in the standard quantum circuit model. We prove, with an additional assumption on the family of gates used in the circuits, that n^2-o(n^{7/4+r}) queries are required, for any r>0. The upper and lower bounds for the standard quantum circuit model are established by pointing out connections with the permutation as substring problem introduced by Karp.

15:30
Propositional Logics Complexity and the sub-formula Property

ABSTRACT. In 1979 Richard Statman proved, using proof-theory, that the purely implicational fragment of Intuitionistic Logic (\mil) is PSPACE-complete. He showed a polynomially bounded translation from full Intuitionistic Propositional Logic into its implicational fragment. By the PSPACE-completeness of S4, proved by Ladner, and the G\"{o}del translation from S4 into Intuitionistic Logic, the PSPACE-completeness of \mil~ is drawn. %% The sub-formula principle for a deductive system for a logic \Log{L} states that whenever ${\gamma_1,\ldots,\gamma_k\}\vdash_{\Log{L}}\alpha$ there is a proof in which each formula occurrence is either a sub-formula of $\alpha$ or of some of $\gamma_i$. In this work we extend Statman's result and show that any propositional (possibly modal) structural logic satisfying a particular statement of the sub-formula principle is PSPACE-complete. As a consequence, EXPTIME-complete propositional logics, such as PDL and the common-knowledge epistemic logic with at least 2 agents satisfy this particular sub-formula principle, if and only if, PSPACE=EXPTIME.

16:00-16:30Coffee Break
16:30-18:00 Session 34S
Location: FH, Seminarraum 138B
16:30
Probabilistic Types and Function Overloading

ABSTRACT. We present a theory of types where, besides the function type, we introduce a new type constructor for probabilistic choice. This constructor allows for the selection of a particular type among a finite set of options according to a given probability. This theory induces a type assignment system for a probabilistic $\lambda$--calculus which we show to be sound with respect to a probabilistic term reduction. We also illustrate the use of this type system in order to express a new form of ad hoc polymorphism, which allows for a probabilistic selection of the code of a polymorphic function to be executed.

17:00
Differential privacy at work: Verification of approximate probabilistic programs and models for choosing epsilon
SPEAKER: unknown

ABSTRACT. This submission surveys some ongoing work on the application of differential privacy—a strong probabilistic privacy guarantee that has recently been under intensive study. We will discuss ideas introduced in previous works, with the overall theme of putting differential privacy to practical use. We have three main goals. First, we wish to explain the concept of differential privacy, and give an idea of why it is useful. Next, from a verification perspective, differential privacy can be seen as an approximate notion of equivalence between probabilistic programs. So, our second goal is to direct attention towards problems related to the probabilitic programming model, which has so far been less explored. Finally, verifying the differential privacy property is only half the challenge—as we will see, the property is parameterized by a numeric value ε, which controls the strength of the guarantee. Hence, a program might be successfully verified to be differentially private, but for an ε that gives a uselessly weak guarantee. Thus, our final, more open-ended goal is to investigate which values of ε give practically useful guarantees, and what this means for verification.

17:30
Interactive Particle Systems and Random Walks on Hypergraphs
SPEAKER: unknown

ABSTRACT. We study hypergraph analogues of interacting particle systems and random walks, notably generalizations of coalescing and annihilating random walks. Their definition is motivated by the problem of analyzing the expected running time of a local search procedure for the $k$-XOR SAT problem, as well as a certain constrained triad dynamics in the theory of social balance.