"Linear Logic Programming" by Chris Martens (2013)

Chris Martens discusses how changing the underlying logic of logic programming to linear logic introduces new programming primitives for state and resources.

Logic programming's core principle, treating proof search as computation, allows for concise and flexible encodings of systems as sets of rules, allowing for search algorithms to leave out the bureauocratic details of state space traversal. By default, most logic programming systems use classical first-order logic as their underlying logic. In this talk, we discuss what new programming primitives are made available by changing the underlying logic to the less-conventional /linear/ logic, in which the unit of meaning is "availability as a resource" rather than "permanent truth". This talk will cover how linear logic programming, via the logical framework and experimental programming language Celf, can be used to capture idioms related to state change and resource usage in a totally declarative fashion. Some possible example applications to be covered: state machines, narrative situations, interactive applications. Chris Martens Carnegie Mellon University @chrisamaphone Chris Martens is a Ph.D. student at Carnegie Mellon University studying logic and programming languages. She is interested in using abstract ivory-tower concepts like type and proof theory for their ability to make high-level ideas quickly executable, and she's working on making those concepts available to creative domains like interactive media and games in addition to more conventional software systems. Recorded at Strange Loop conference (thestrangeloop.com) in St. Louis, MO, Oct 2013.