Lambda the Ultimate

You might still apply for a grant, but time is short!

Only a tentative program is currently available, but I suppose the topics mentioned in it will remain in the final program, and many of them are interesting, and often discussed here on LtU.

We exhibit the rationale behind the design of Epigram, a dependently typed programming language and interactive program development system using refinements of a well known program, merge sort, as a running example. We discuss the relationship to other proposals to introduce aspects of dependent types into functional programming languages and sketch some topics for further work in this area.

Epigram, dependent types, general reucrsion, indexed datatypes - it's all here!

Enjoy.

Although I really just lurk I have to say I really like what this site is doing - providing a modern web community that focuses on certain areas of academic research and unites to some degree various academics, professionals, interested students and hobbyists. Provides interesting papers, references, news and discussion.

Perhaps this is just a symptom of the fact that computer scientists are likely to be a lot more clued up about the web and its uses than your average academic - although hopefully this will change and these sorts of things will become widespread.

What I'm asking is - does anyone know of any other sites doing something similar for other academic areas? I'd be particularly interested in any mathematics-related sites with a similar ethos, although any areas really!

Since I know there are many CT enthusiasts here at LtU, I thought I would share news of the passing of Saunders Mac Lane, one of the giants of the field, and of modern mathematics in general.

Here is an obituary.

Distributed systems and applications are often expected to enforce high-level authorization policies. To this end, the code for these systems relies on lower-level security mechanisms such as, for instance, digital signatures, local ACLs, and encrypted communications. In principle, authorization specifications can be separated from code and carefully audited. Logic programs, in particular, can express policies in a simple, abstract manner. For a given authorization policy, we consider the problem of checking whether a cryptographic implementation complies with the policy. We formalize authorization policies by embedding logical predicates and queries within a spi-calculus. This embedding is new, simple, and general; it allows us to treat logic programs as specifications of code using secure channels, cryptography, or a combination. Moreover, we propose a new dependent type system for verifying such implementations against their policies. Using Datalog as an authorization logic, we show how to type several examples using policies and present a general schema for compiling policies.

I guess it's dependent types day around here...