Skip to main content

Posts

Showing posts from May, 2014

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 rules (such as tensor left), and moreso because they…

Paper draft: Generative Story Worlds as Linear Logic Programs

I'm pleased to announce that João Ferreira, Anne-Gwenn Bosser, and I have had a paper accepted at (INT)7! I've made a draft available (7 page pdf), though some parts may read a bit strangely with reference to our prior work, since the original submission was anonymized. (This was my first experience with double-blind reviewing, and, well, I suppose all current data places me in favor. ;) )
Abstract:

Linear logic programming languages have been identified in prior work as viable for specifying stories and analyzing their causal structure. We investigate the use of such a language for specifying story worlds, or settings where generalized narrative actions have uniform effects (not specific to a particular set of characters or setting elements), which may create emergent behavior through feedback loops.
We show a sizable example of a story world specified in the language Celf and discuss its interpretation as a story-generating program, a simulation, and an interactive narrative…