2024-10-16

Curry-Howard correspondences between Linear Logic (LL) and session types provide a firm foundation for concurrent processes. As the correspondences hold for intuitionistic and classical versions of LL (ILL and CLL), we obtain two different families of type systems for concurrency. An open question remains: how do these two families exactly relate to each other? Based upon a translation from CLL to ILL due to Laurent, we provide two complementary answers, in the form of full abstraction results based on a typed observational equivalence due to Atkey. Our results elucidate hitherto missing formal links between seemingly related yet different type systems for concurrency.

(based on joint work with Dan Frumin and Jorge Pérez, presented at CONCUR'24)

We show in this talk that the problem of deciding the consequence relation of the full Lambek calculus with weakening is complete for the class HAck of hyper-Ackermannian problems (i.e., level ω^ω of the ordinal-indexed hierarchy of fast-growing complexity classes). Provability was already known to be PSPACE-complete. We will see that this problem is HAck-complete even for the multiplicative fragment. Lower bounds are proved via a novel reduction from reachability in lossy channel systems and the upper bounds are obtained by combining structural proof theory (forward proof search over sequent calculi) and well-quasi-order theory (length theorems for Higman's Lemma).

Guarded Kleene Algebra with Tests (GKAT) provides a sound and complete framework to reason about trace equivalence between simple imperative programs. It is completely agnostic with respect to the meaning of primitives (keep equivalence decidable) and excludes non-local control flow such as goto, break and return. This limits its application to real-world programs. We introduce control flow GKAT (CF-GKAT), a system that allows control-flow equivalence checking of programs that include non-local control flow as well as hardcoded values.

CF-GKAT is able to soundly and completely verify trace equivalence of a larger class of programs, while preserving the efficiency of GKAT. This makes CF-GKAT suitable for the verification of control-flow manipulating procedures, such as decompilation and goto-elimination. To demonstrate CF-GKAT's abilities, we validated the output of several highly non-trivial program transformations, such as Böhm-Jacopini conversion, and Erosa and Hendren's goto-elimination procedure.