Papers I'm reading

Here is an incomplete selection of some good papers I'm currently reading:

• Constructing Type Systems over an Operational Semantics, Robert Harper.
• A Realizability Interpretation of Martin-Loef Type Theory, Catarina Coquand.

  These two papers give a very nice introduction to developing the metatheory of dependent type systems. Harper's paper is about extensional type theory, and Coquand's is about intensional type theory, but IMO they both demonstrate the benefits of using realizability to formulate the semantics of type theory -- they are both impressively simple, given the complexity of the type theories involved.

• Categorical Glueing and Logical Predicates for Models of Linear Logic, Masahito Hasegawa.

  This is another paper on logical relations, this time for linear logic. This is one of the papers that has made me seriously interested in classical linear logic for the first time. Basically, the "double glueing" construction used to formulate models to CLL looks a bit like the notion of "biorthogonality" or "TT-closure" sometimes to interpet higher-order programming languages, but with some very intriguing differences.

  Pitts's Parametric Polymorphism and Operational Equivalence is a good introduction to biorthogonality, though the actual origins of the idea are a bit mysterious to me. At any rate, the idea is that if you have a program value, then its "orthogonal" is the set of continuations which won't crash when supplied the value as an argument. Similarly, if you have a continuation, then its orthogonal is the set of values that won't crash the continuation. So if you take a set of values, and then take their orthogonal, and then take their orthogonal again, you have a new, potentially bigger, set of values. A "biorthogonal" is a set of values which remains the same when you take its double orthogonal. This means you can equivalently think of a set of values as the set of continuations which accept it, which is often quite convenient for defining the meaning of a type.

  With double glueing, you again think of a type in as a set of values which make it up, and a set of continuations it can supply. But unlike with biorthogonality, there is no procedure for constructing the continuations from the values or vice-versa --- instead, you get to define the values and the continuations as anything you like, as long as everything plays nicely together. This extra degree of freedom is really intriguing, and I'm curious what can be done with it.