Lambda the Ultimate

In my eternal quest for provably safe concurrent and distributed resource management, I'm trying to reach an understanding of dependent types. I have read a bit about them, even toyed a little bit with them in Twelf, but I still don't quite *get* them.

• Really, what *are* dependent types ? What do we expect to do with them ? Where exactly does the domain stop ?
• Have DML, Cayenne, Epigram been tested with pragmatic examples, beyond simple lists manipulation ? -- I don't include Twelf or Coq in the list as the focus of these languages is quite different.
• What are the limitations of dependent types ? Is typechecking even decidable ?
• How much of dependent typing can be encoded with non-dependent types ?
• Are there works on dynamic counterparts of dependent types ?
• What papers/tutorials must one absolutely read on the subject ?

By the way, the Wikipedia article on Dependent Types is nearly empty. Is there anyone interested in completing it ?

In the beginning was game semantics

Giorgi Japaridze

[...] the story and philosophy of computability logic (CL) [...]
According to its philosophy, syntax — the study of axiomatizations or any other, deductive or nondeductive string-manipulation systems — exclusively owes its right on existence to semantics, and is thus secondary to it. CL believes that logic is meant to be the most basic, general-purpose formal tool potentially usable by intelligent agents in successfully navigating real life. And it is semantics that establishes that ultimate real-life meaning of logic. Syntax is important, yet it is so not in its own right but only as much as it serves a meaningful semantics, allowing us to realize the potential of that semantics in some systematic and perhaps convenient or efficient way.
[...]
the philosophy of CL relies on two beliefs that, together, present what can be considered an interactive version of the Church-Turing thesis:

Belief 1.

The concept of static games is an adequate formal counterpart of our intuition of ("pure", speed-independent) interactive computational problems.

Belief 2.

The concept of winnability is an adequate formal counterpart of our intuition of algorithmic solvability of such problems.

I already posted links to papers of Giorgi Japaridze several times, but most of them were pretty technical, and also that was before the latest expansion of LtU's readership.

In short, CL is about trying to generalize traditional (both classical and intuitionistic) logic beyond batch computation (well, I hope everybody knows why logic is relevant to computation, if not - look for Curry-Howard isomorphism, or CHI). There are several approaches to doing that, but Giorgi believes they go the wrong way by trying to build upon the syntax, while it's semantics that is primary.

If you believe that computation is more than calculating a function, and that logic is a good way to understand computation - then I recommend to read at least the introduction and the references' list of this paper (the paper is a single chapter for a book, would love to see the whole book).