Zoo of term assignments for linear sequent calculus
It's pretty common to give term assignments to logics presented through natural deduction. We usually call them "(typed) functional programming languages." What's less common, though possible, is to give a term assignment to sequent representations. I've come across enough of these for linear logic in particular that I can make a little petting zoo for you. Terms as concurrent processes , from Caires, Pfenning, and Toninho's Session Types : Terms as stories (or more accurately, narrative structures), from Bosser, Cortieu, Forest, and Cavazza's " Structural Analysis of Narratives with the Coq Proof Assistant ": Terms as plans , from Cresswell, Smail, and Richardson's " Deductive Synthesis of Recursive Plans in Linear Logic " (paywall warning, but searching those terms also turns up a .ps.gz): The latter two are especially interesting to me because (a) they elide term markers for certain ru