A Very Modal Model of a Modern, Major, General Type System

A Very Modal Model of a Modern, Major, General Type System, by Andrew W. Appel, Paul-Andre Mellies, Christopher D. Richards, and Jerome Vouillon. Preliminary version of August 10, 2006.

We wish to compile languages such as ML and Java into typed intermediate languages and typed assembly languages. These TILs and TALs are particularly difficult to design, because in order to describe the program transformations applied in the course of compilation, they require a very rich and expressive type system... Putting all these type ingredients together in a low-level language is an intricate exercise. A formal proof of soundness —any well-typed program does not go wrong—is thus recommended for any type system for such TILs and TALs.

It has been awhile since we discussed work in this area. The current paper is quite intriacte, it seems, and I don't have the time to read it carefully. Maybe someone else would care to elaborate. The paper makes a few technical innovations, and uses several interesting techniques. Soundness is not proved syntactically, but rather semantically.

Some LtU member will be happy to see that the authors use Coq to formalize their proofs.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

I'm disappointed the

I'm disappointed the abstract isn't in iambic octameter.

Gilbert would have been proud!

Gilbert would have been proud! (...or turning in his grave.)

Paper of the month

For the title alone... I haven't read it yet.


I haven't read the paper yet, but I agree that the title alone is priceless. And yes, it's gratifying that more people are seeing the value of tools to help with formalization, whether it's Coq or Twelf or what have you.


This is the first paper I've seen that explicitly defines universal quantifiers and existential quantifiers as dependent type intersections and unions indexed over the quantifier's domain type. (Is this fact obvious to type theorists? It took me quite a lot of stumbling to recognize the connection myself.) There are a lot of other interesting things to be found in this paper. It's been clear to me for a while that implementing proof-carrying code on top of mainstream (powerful and complex) programming languages will require something quite a lot like the system described here.

Quantifiers and Dependent Types

I hadn't seen the connection (between quantifiers and dependent types) either until a couple of days ago when I first worked my way through the Coq tutorial that was posted in one of the comments.

From the tutorial:

"Actually, universal quantification, implication, as well as function formation, are all special cases of one general construct of type theory called dependent product."

Re: Quantifiers

Is this fact obvious to type theorists?

I'm no expert in Martin-Löf type theory, but I think it's well-known. You might try

@incollection{ barendregt92lambda,
    author = "Henk Barendregt",
    title = " Lambda Calculi with Types ",
    booktitle = "Handbook of Logic in Computer Science, Volumes 1 (Background: $
    volume = "2",
    year = "1992",
    url = "citeseer.nj.nec.com/barendregt92lambda.html" }

or Simon Thompson's textbook.

There seem to be a couple more references in this LtU thread.

Goedel-Loeb logic

Only just skimmed the abstract & intro, but what I've skimmed suggests logical depth: wondering what sense of "modal" the title alluded to, I see that they use the Goedel-Loeb logic of provability to give them a means of capturing properties that hold over any finite number of reductions without the (notationally & computationally) expensive formal overhead of using quantification over classes of reduction paths. Not an original insight, but not a widely known trick either: it adds a touch of class. I look forward to finding time to look over this paper properly...

It seeme that the SEP has a

It seems that the SEP has a nice entry on Provability Logic. I am not sure what would be a good (online) starting point for those interested in Modal Logic, possible world semantics and Kripke structures, since my route to this topics was a bit strange (it all began with distributed algorithms and the classic book Reasoning about Knowledge... Well, maybe it did not begin there, since I did know some modal logic before, but it was a big step).

A new one for the Papers section?

It may be too soon to tell, but having finally gotten around to reading this paper more fully, I had that feeling you get when you feel like you've just read a soon-to-be seminal paper in the field.

Any one else share that feeling? (Or did I just have too much caffeine today? ;-))