Lambda the Ultimate

Martin-Löf's Type Theory (M-LTT) was developed by Per Martin-Löf in the early 1970s, as a constructive foundation for mathematics. The theory is clear and simple. Because of this it has been used for everything from program derivation to handling donkey sentences.

In this talk we will present and give a flavour of Martin-Löf's Type Theory. We will highlight the use of proof theoretical justification of the rules, without explaining this in full detail. We will present the rules for various types, emphasising the uniformity of the presentation. The types that we will present will include those needed to express the logical constants falsum, or, and, not, implies, for all, and there exists.

Yet another propositions-as-types tutorial.

It seems pretty easy to follow, and it is quite short (16 pages).

P.S

Why all the theory on LtU these days? Because the editors who keep posting are into theory. The other editors should be nudged to start posting cool hands-on stuff...

A number of effective error detection tools have been built in recent years to check if a program conforms to certain design rules. An important class of design rules deals with sequences of events associated with a set of related objects. This paper presents a language called PQL (Program Query Language) that allows programmers to express such questions easily in an application-specific context. A query looks like a code excerpt corresponding to the shortest amount of code that would violate a design rule. Details of the target application's precise implementation are abstracted away. The programmer may also specify actions to perform when a match is found, such as recording relevant information or even correcting an erroneous execution on the fly. We have developed both static and dynamic techniques to find solutions to PQL queries. Our static analyzer finds all potential matches conservatively using a context-sensitive, flow-insensitive, inclusion-based pointer alias analysis. Static results are also useful in reducing the number of instrumentation points for dynamic analysis. Our dynamic analyzer instruments the source program to catch all violations precisely as the program runs and optionally to perform user-specified actions. We have implemented techniques described in this paper and used this combination of static and dynamic analysis to successfully find 206 breaches of security and important resource leaks in 6 large real-world open-source Java applications containing a total of nearly 60,000 classes.

I saw the talk to this paper two weeks ago at OOPSLA two weeks ago and liked it very much. In a sense, I would consider it as a new application for aspect-oriented techniques.