Home

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.

By Ehud Lamm at 2006-10-08 13:16 | Implementation | Type Theory | other blogs | 78990 reads

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.

By Doug Orleans at Sun, 2006-10-08 20:21 | login or register to post comments

Gilbert would have been proud!

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

By Kaushik Sridharan at Mon, 2006-10-09 03:30 | login or register to post comments

Paper of the month

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

By plragde at Mon, 2006-10-09 16:27 | login or register to post comments

Heh

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.

By Paul Snively at Tue, 2006-10-10 16:54 | login or register to post comments

Quantifiers

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.

By Tim Sweeney at Tue, 2006-10-10 17:31 | login or register to post comments

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."

By Gavin Mendel-Gleason at Tue, 2006-10-10 18:57 | login or register to post comments

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.

By Dave Herman at Tue, 2006-10-10 19:21 | login or register to post comments

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...

By Charles Stewart at Tue, 2006-10-10 20:39 | login or register to post comments

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).

By Ehud Lamm at Wed, 2006-10-11 10:02 | login or register to post comments

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? ;-))

By Marc Hamann at Wed, 2006-11-08 20:17 | login or register to post comments