Lambda the Ultimate

I am new to FP and have been struggling on an on & off basis for over a year now. I think now I have at least an elementary hold on various facets of the field. My interest lies primarily in theoretical & formal computer science. So could somebody please recommend me which language would be most suitable for my purposes??I mean it should help me grasp the underlying mathematics without getting me diverted into how it can be helpful in implementing "real" projects.

I know something of haskell and am now beginning ML. And have advanced knowledge of C#.Net including the functional extensions in version 3.0. Some pointers as to useful web tutorials or books will also be great.

thanking in advance
Barun

Eriskay: a Programming Language Based on Game Semantics. John Longley and Nicholas Wolverson. GaLoP 2008.

We report on an ongoing project to design a strongly typed, class-based object-oriented language based around ideas from game semantics. Part of our goal is to create a powerful modern programming language whose clean semantic basis renders it amenable to work in program verification; however, we argue that our semantically inspired approach also yields benefits of more immediate relevance to programmers, such as expressive new language constructs and novel type systems for enforcing security properties of the language. We describe a simple-minded game model with a rich mathematical structure, and explain how this model may be used to guide the design of our language. We then focus on three specific areas where our approach appears to offer something new: linear types and continuations; observational equivalence for class types; and static control of the use of higher-order store.

In a substantial appendix, we present the formal definition of a fragment of our language which embodies many of the innovative features of the full language.

It's always interesting to see a new programming language strongly based on some mathematical formalism, because a language gives you a concrete example to match the abstract semantic definitions to, and game semantics is something that I've been curious about for a while.

One particularly interesting feature is that the core language has a restricted model of the heap, which controls the use of higher-order store in such a way that cycles are prohibited. This is enforced with a notion called "argument safety", which essentially prohibits storing values of higher type into fields which come from "outside" the object. This is somewhat reminiscent of the ownership disciplines found in OO verification systems like Boogie, which enforce a tree structure on the ownership hierarchy. It would be very interesting to find out whether this resemblance is a coincidence or not.

(Samson Abramsky has some lecture notes on game semantics for the very curious.)

Writing practical memory management code with a strictly typed assembly language, by Toshiyuki Maeda, and Akinori Yonezawa.

Memory management (e.g., malloc/free) cannot be implemented in traditional strictly typed programming languages because they do not allow programmers to reuse memory regions, in order to preserve memory safety. Therefore, they depend on external memory management facilities, such as garbage collection. Thus, many important programs that require explicit memory management (e.g., operating systems) have been written in weakly typed programming languages (e.g., C). To address the problem, we designed a new strictly and statically typed assembly language which is flexible and expressive enough to implement memory management. The key idea of our typed assembly language is that it supports variable-length arrays (the arrays whose size is not known until runtime) as language primitives, maintains integer constraints between variables, and keeps track of pointer aliases. Based on the idea, we implemented a prototype implementation of the language. We also implemented a small operating system kernel which provides a memory management facility with the language.

This paper forms part of Toshiyuki Maeda's thesis, where he also uses TALK (OCaml source code available) to build a certified x86 kernel called TOS (source code available). I'm surprised I hadn't heard of this work before, as it seems quite practical.

The paper does not discuss the limitations of TALK, though the thesis does. The most significant disadvantage is described in section 2.8.1:

The type system of TALK is flexible and expressive enough to implement practical memory management code (e.g., malloc/free). However, it is not enough to efficiently implement all the data structures that can be represented in ordinary typed languages, because the type system of TALK restricts pointer manipulation in some cases in order to keep track of aliasing relations between pointers. For example, generic graph data structures including directed acyclic graphs and cyclic graphs cannot be represented naturally in the type system of TALK. This is because once a memory region is encapsulated inside an existential package, the region cannot be accessed until the package is unpacked.

They suggest prior work designed to relax linearity restrictions can be applied to TALK to enable graph structures to be captured.

While TALK is a low-level assembly language, other higher level languages have attempted to capture safe low-level memory management as well.