Superficially Substructural Logic

Together with Aaron Turon, Derek Dreyer, and Deepak Garg as coauthors, we have a new draft paper out: Superificially Substructural Types.

Many substructural type systems have been proposed for controlling access to shared state in higher-order languages. Central to these systems is the notion of a resource, which may be split into disjoint pieces that different parts of a program can manipulate independently without worrying about interfering with one another. Some systems support a logical notion of resource (such as permissions), under which two resources may be considered disjoint even if they govern the same piece of state. However, in nearly all existing systems, the notions of resource and disjointness are fixed at the outset, baked into the model of the language, and fairly coarsegrained in the kinds of sharing they enable.

In this paper, inspired by recent work on “fictional disjointness” in separation logic, we propose a simple and flexible way of enabling any module in a program to create its own custom type of splittable resource (represented as a commutative monoid), thus providing fine-grained control over how the module’s private state is shared with its clients. This functionality can be incorporated into an otherwise standard substructural type system by means of a new typing rule we call the sharing rule, whose soundness we prove semantically via a novel resource-oriented Kripke logical relation.

I'm very excited by this work, since this paper represents a big step towards a longstanding research goal of mine: generalizing separation logic so that resource abstractions can be defined by the programmer on a per-module basis.

Michael Dummett

The British philosopher Michael Dummett's books The Logical Basis of Metaphysics and Frege: Philosophy of Language were some of the most useful books I read during my degree. His analysis of Frege's sense-reference distinction has been very helpful to my understanding of dependent type theory, and his explanation of intuitionism was quite helpful in understanding the relationship between the structural-proof-theoretic view of types and the realizability interpretation of types.

So I was disappointed to learn that he died last week, but pleased  to read the reminiscences of him by his colleagues posted on the New York Times.

Adding Equations to System F, at ESOP 2012

Our paper on adding equations to system F was accepted to ESOP 2012!

The reviewers suggested rather a lot of improvements to the paper, so I'm taking the draft down while we incorporate their suggestions. It will go up again in a few weeks, after the revisions are done, and undoubtedly in a much-improved state. 

Updata

The final version of our POPL paper on space-bounded FRP is available now -- we bought two extra pages from the ACM, and used them to add a lot more detail to the examples. With luck the paper will be a lot clearer now.

Also, Bob Atkey has a new blog post on using delay operators to model guarded definitions in type theory. He takes advantage of the fact that delay is a strong lax monoidal functor (with respect to the monoidal structure of products) to use the syntax of applicative functors.

This is a very elegant way of embedding these things into Haskell. Unfortunately, I have never liked the typing rules for the idiom syntax, since they don't work solely on the outermost type constructor. This means type-theoretic properties like normalization are messier to prove. (Bob evades this problem with semantic techniques, though.)


All his other posts are very good, too.

Adding Equations to System F

Nick and I have a new draft out, on adding types for term-level equations to System F. Contrary to the experience of dependent types, this is not a very hairy extension -- in fact, I would not even hesitate to call it simple.

However, it does open the door to all sorts of exciting things, such as many peoples' long-standing goal of putting semantic properties of modules into the module interfaces. This is good for documentation, and also (I would hope) good for compilers --- imagine Haskell, if the Monad typeclass definition also told you (and ghc!)  all the equational rewriting that it was supposed to do.

Higher-Order Functional Reactive Programming in Bounded Space

I just learned that our (with Nick Benton and Jan Hoffmann) paper, Higher-Order Functional Reactive Programming in Bounded Space, was accepted for publication at POPL 2012!

I am very happy with this work, since it resolves some of the thorniest problems in FRP (memory usage and space leaks) without giving up the highly expressive higher-order abstractions that makes FRP attractive in the first place.

A technical surprise in this work is that this stuff is the first place I've seen where the magic wand of separation logic is actually essential. The denotational model in this paper is a variation on Martin Hofmann's length space model, which forms a doubly-closed category modelling bunched implications. In this paper, we needed both function spaces: we needed the linear function space to control allocation, and we needed the ordinary function space to make use of sharing.

It would be interesting to see if there are ways to transport some of these ideas back to Hoare-style separation logic to find some interesting new invariants.

Radical predicativism

This isn't really on-topic for this blog, but I can't resist posting this: the Princeton mathematician Edward Nelson claims to have found an inconsistency in arithmetic! On the FOM mailing list, he posted:

I am writing up a proof that Peano arithmetic (P), and even a small fragment of primitive-recursive arithmetic (PRA), are inconsistent. This is posted as a Work in Progress at http://www.math.princeton.edu/~nelson/books.html

A short outline of the book is at:

http://www.math.princeton.edu/~nelson/papers/outline.pdf

The outline begins with a formalist critique of finitism, making the case that there are tacit infinitary assumptions underlying finitism. Then the outline describes how inconsistency will be proved. It concludes with remarks on how to do modern mathematics within a consistent theory.

There's some discussion of this at The n-Category Cafe, including a brief (so far) discussion between Terry Tao and Nelson himself. Obviously, I expect a flaw will be found in his proof -- but I sure hope he's right! That would mean all of mathematics will be in need of revision.

Update: Nelson says that Tao has indeed found a hole in the proof. Exponentiation remains total, for now.