Post #2660341

What if the core insight of Duff's rc shell (Plan 9, Bell Labs), taking the sequence instead of strings as the primitive object, can be interpreted with virtual double categories as the semantic frame and sequent calculus as the type theory of its morphisms? I'm not entirely sure yet, but I am optimistic about what may lie in this interpretation for the shell, an often maligned setting of computation.