Interactivity, week 2
My post about week 1 established a new research project I'm working on involving programming interactivity with substructural logic. This past week, I've been working on digesting some background and related work. One thing I did was spend a good long stretch working through the core ideas in Yuxin, Iliano, and Rob's paper Relating Reasoning Methods in Linear Logic and Process Algebra . Linear contexts as processes The point of the paper is to establish that a so-called "logical preorder" on contexts \[ \Delta \preceq_l \Delta' \] defined (I'm simplifying to the strictly linear case 1 ) as \[ {For}\ {all}\ C, \Delta \vdash C \ {implies}\ \Delta' \vdash C \] where \[ \vdash \] is entailment in linear logic, corresponds to traditional notions of contextual preorder in CCS/process algebras, which are defined coinductively by a reduction relation extended over a laundry list of structure-preserving properties. The symmetric closure of th...