We establish a tight connection between two models of the $λ$-calculus, namely Milner's encoding into the $π$-calculus (precisely, the Internal $π$-calculus), and operational game semantics (OGS). We first investigate the operational correspondence between the behaviours of the encoding provided by $π$ and OGS. We do so for various LTSs: the standard LTS for $π$ and a new `concurrent' LTS for OGS; an `output-prioritised' LTS for $π$ and the standard alternating LTS for OGS. We then show that the equivalences induced on $λ$-terms by all these LTSs (for $π$ and OGS) coincide. We also prove that when equivalence is based on complete traces, the `concurrent' and `alternating' variants of OGS also coincide with the `well-bracketed' variant. These connections allow us to transfer results and techniques between $π$ and OGS. In particular: we import up-to techniques from $π$ onto OGS; we derive congruence and compositionality results for OGS from those of $π$; we transport the notion of complete traces from OGS onto $π$, obtaining a new behavioural equivalence that yields a full abstraction result for the encoding of $λ$-terms with respect to contexts written in a $λ$-calculus extended with store. The study is illustrated for both call-by-value and call-by-name.
Timed automata (TAs) are an extension of finite automata that can measure and react to the passage of time, providing the ability to handle real-time constraints using clocks. In 2009, Franck Cassez showed that the timed opacity problem, where an attacker can observe some actions with their timestamps and attempts to deduce information, is undecidable for TAs. Moreover, he showed that the undecidability holds even for subclasses such as event-recording automata. In this article, we consider the same definition of opacity, by restricting either the system or the attacker. Our first contribution is to prove the inter-reducibility of two variants of opacity: full opacity (for which the observations should be the same regardless of the visit of a private location) and weak opacity (for which it suffices that the attacker cannot deduce whether the private location was visited, but for which it is harmless to deduce that it was not visited); we also prove further results including a connection with timed language inclusion. Our second contribution is to study opacity for several subclasses of TAs: with restrictions on the number of clocks, the number of actions, the nature of time, or a new subclass called observable event-recording automata. We show that opacity is mostly decidable in these cases, except for one-action TAs and for one-clock TAs with $ε$-transitions, for which undecidability remains. Our third (and arguably main) contribution is to propose a new definition of opacity in which the number of observations made by the attacker is limited to the first $N$ observations, or to a set of $N$ timestamps after which the attacker observes the first action that follows immediately. This set can be defined either a priori or at runtime; all three versions yield decidability for the whole TA class.
The article studies query evaluation in parallel constant time in the CRCW PRAM model. While it is well-known that all relational algebra queries can be evaluated in constant time on an appropriate CRCW PRAM model, this article is interested in the efficiency of evaluation algorithms, that is, in the number of processors or, asymptotically equivalent, in the work. Naive evaluation in the parallel setting results in huge (polynomial) bounds on the work of such algorithms and in presentations of the result sets that can be extremely scattered in memory. The article discusses some obstacles for constant-time PRAM query evaluation. It presents algorithms for relational operators and explores three settings, in which efficient sequential query evaluation algorithms exist: acyclic queries, semijoin algebra queries, and join queries -- the latter in the worst-case optimal framework. Under mild assumptions -- that data values are numbers of polynomial size in the size of the database or that the relations of the database are suitably sorted -- constant-time algorithms are presented that are weakly work-efficient in the sense that work $\mathcal{O}(T^{1+\varepsilon})$ can be achieved, for every $\varepsilon>0$, compared to the time $T$ of an optimal sequential algorithm. Important tools are the algorithms for approximate prefix sums and compaction from Goldberg and Zwick (1995).
When working in a proof assistant, automation is key to discharging routine proof goals such as equations between algebraic expressions. Homotopy type theory allows the user to reason about higher structures, such as topological spaces, using higher inductive types (HITs) and univalence. Cubical type theory provides computational support for HITs and univalence. A difficulty when working in cubical type theory is dealing with the complex combinatorics of higher structures, an infinite-dimensional generalisation of equational reasoning. To solve these higher-dimensional equations consists in constructing cubes with specified boundaries. We develop a simplified cubical language in which we isolate and study two automation problems: contortion solving, where we attempt to "contort" a cube to fit a given boundary, and the more general Kan solving, where we search for solutions that involve pasting multiple cubes together. Both problems are difficult in the general case-Kan solving is even undecidable-so we focus on heuristics that perform well on practical examples. Our language encompasses different variations of cubical type theory which differ in their "contortion theory", i.e., the class of contortions they support. We provide a solver for the contortion problem for the most complex contortion theories currently being researched, the Dedekind and De Morgan contortions, by utilizing a reformulation of contortions in terms of poset maps. We solve Kan problems using constraint satisfaction programming, which is applicable independently of the underlying contortion theory. We have implemented our algorithms in an experimental Haskell solver that can be used to automatically solve many goals a user of cubical type theory might face. We illustrate this with a case study establishing the Eckmann-Hilton theorem using our solver, as well as various benchmarks.
We show that certain diagrams of $\infty$-logoses are reconstructed in homotopy type theory extended with some lex, accessible modalities, which enables us to use plain homotopy type theory to reason about not only a single $\infty$-logos but also a diagram of $\infty$-logoses. This also provides a higher dimensional version of Sterling's synthetic Tait computability -- a type theory for higher dimensional logical relations.
