View: session overviewtalk overviewside by side with other conferences

09:15 | Numeral Systems in the Lambda Calculus SPEAKER: Ian Mackie ABSTRACT. We investigate numeral systems in the λ-calculus; specifically |

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 | Quantitative semantics for higher-order probabilistic and quantum computation SPEAKER: Michele Pagani ABSTRACT. 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. |

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 SPEAKER: Edward Hermann Haeusler 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:30 | Probabilistic Types and Function Overloading SPEAKER: Alessandra Di Pierro 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. |