Everything in Context

Conor McBride posted a really intriguing list of research problems on his mind at the end of this year, and I thought it was an amazing idea, so I'm copying it. I have little notes I've made to myself in paper notebooks and text files, but rarely do I go through and collect them all in one place. Computer-checking linear logic program invariants (and other, perhaps variant, properties) - what is an appropriate metalogic to reason about linear proof search? Generative invariants : what is their expressive range? Does it have something to do with (co)inductive datatypes or their dependent generalization? Can we extend them to describe general structures such as graphs (with no self-edges or multi-edges), perhaps by allowing quantification over, and introduction to, *sets* of terms rather than types? Ordered logic - are there more connectives? constrained replication and mobility, e.g. a propositional operator *A meaning A can be replicated "in place." What type

Let's talk about execution traces of concurrent programs, and which ones we consider "the same." In concurrent programming models, your program constructs allow you to specify computation as indexed by a particular independent execution unit ("thread", "channel", "actor" -- at this level of detail, we can use these terms interchangeably), and to specify how those units communicate or interact. This means you have one artifact, the static program, that gives rise to a set of traces , or possible executions -- records of which parts of the program were evaluated in what order. We might say that if this set of program traces has only one element, then the program is sequential . But the accuracy of this statement depends on how exactly we represent a program trace! If we are forced to give a total ordering on all computation steps -- unifying a trace with an "interleaving of instructions" -- then yes, the only class of programs for

My friend Jim just told me about an exciting-sounding internship opportunity for Ph.D. students in programming languages! Check it out: Disney Research Pittsburgh seeks a PhD student with experience in Programming Languages or Compilers for a summer internship. The student will be expected to apply programming language methods to the analysis and control of knitting machines, with potential topics including:   developing a semantics for machine knitting   formally describing a notion of machine knittability   inverse knitting   knit scheduling   knitting pattern optimization   knitting failure analysis and robustness estimation   translation from hand knitting to machine knitting As part of the internship, the student will write up their work for submission to an appropriate top-tier venue; applicants with prior publications in such venues will be strongly favored. Interested students should contact Jim McCann (jmccann@disneyresearch.com) to arrange a further conver

I just read this  blog series on "purely functional retrogames"  from six years ago, on the basis of a recommendation from my Twitter friend/occasional conference-co-attendee  Scott Vokes . Things I thought were interesting points/good takeaways: It's better to nest state-keeping records deeply, rather than making wide/flat ones; never have more than a few fields to refer to, and you can pass around chunks at a time to different subroutines. Being forced to think out data-dependencies can be a good thing: [In a purely functional style], functions can't access any data that isn't passed in. That means you need to think about what data is needed for a particular function, and "thread" that data through your program so a function can access it. It sounds horrible when written down, but it's easy in practice.  In fact, just working out the data dependencies in a simple game is an eye-opening exercise. It usually turns out that there are far f

[This is a post about game/interactive narrative design theory. If you're here for the logic and type theory, there won't be much of that in this post.] Many of the games that interest me, including my own experiments , play with the idea of focalization in a narratology sense,* which is essentially a generalization/reformulation of the idea of "perspective" in literature (which should call to mind the terms "first/second/third person," for example). In particular, in settings where multiple agents (loosely construed as "entities in a game with somehow separable trajectories in state space") can act and interact, independently or interdependently, there is a huge space of design decisions to be made. In this post I'm going to describe a design space for multi-agent games as context for reflecting on two projects I worked on recently, the IFComp entry  Origins  and the  PROCJAM  entry Quiescent Theater . Focalization in Games Quick run

My last post described the idea of concurrent storytelling  to encapsulate the idea of narrative structures where simultaneous action can lead to multiple experiences of a story, either through nondeterminism or through differing sequential traversals of the story graph. Since then, I have obtained a copy of the Tamara  script (which is written like a really bizarre choose-your-own-adventure book) and begun transcribing its scene structure as a deterministic Celf program such that the output trace models the scene dependency graph. To do this, I model each of the 10 characters as a predicate over a location and a scene identifier, e.g. tamara : scene -> location -> type. The scene IDs roughly correspond to the letter-and-numbered scenes in the script, except that they are slightly finer grained to accommodate the different perspectives induced by character entrances and exits, although those entrances/exits are contained within a single script-scene. In the simple case

This post outlines one way of understanding what my thesis is about: a tool for concurrent storytelling . For this post, I'll speak mainly in terms of narrative structure & system design rather than PL & logic. My goal is that an audience more oriented in interactive fiction than in programming languages can follow along. Please feel free to send me feedback about the accessibility of this writing from that perspective! Previously, I've described my thesis programming language as a tool for designing game mechanics . But the term "game mechanics" is fairly broad, and in my proposal , I gave examples ranging from 2d puzzle games to parser interactive fiction. While I'm still excited about designing a core language that can express that entire range of mechanics, I've also narrowed my focus somewhat to examples that are especially illuminating to design this way. In my INT 7 paper presented in June, I wrote about what I identified as the first solid

Before I begin the technical content of this post, just a quick update: I gave my talk on "Generative Story Worlds as Linear Logic Programs" at INT in Milwaukee on the 17-18th, and I kept a travelogue, which includes notes from all the talks! The travelogue also details my time at AdaCamp, an "unconference" event on feminism & open technology, which I would strongly recommend to any women interested in those topics. I had a great time meeting people at both of these events! -- Where I  last left off  in my discussion of the event calculus, I was discussing the idea of "encoding" vs. "embedding." In some discussions, these terms map onto the alternate terms "deep embedding" and "shallow embedding." If I understand them correctly, Alexiev's program gives a deep embedding of the event calculus: the core constructs of the calculus, fluents and events, are modeled as terms in the underlying logic program. I was

My research uses linear logic to describe actions , i.e. to write rules to answer the question "what happens if..." rather than "what holds if...". The desire to reason about actions follows a long line of endeavors to create AI with logic, where back then AI seemed to mean "computational agents that can take initiative, have goals, reason about their environments, and act upon them." AI-inspired logicians have been reasoning about actions for a long time, and one fruitful tool for doing so is the Event Calculus ( Kowalski and Sergot 1986 ). In this post, I'm going to describe my understanding of the relationship between Event Calculus and linear logic, by way of some Celf code I wrote last week after reading Vladimir Alexiev's " Event Calculus as a Linear Logic Program ." Primarily, this is a post about that particular paper and the tinkering I did around it, but I'll also explain some of the context I've picked up on the way.

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

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 n