Lambda the Ultimate

Ideally, I'd love to find something like Wilson's GC survey, covering everything from various low level mechanisms such as raw thread/lock manipulation, condition variables, etc. up to much more programmatic stylized idiomatic approaches to concurrency - Erlang style actors, internal pipes or what I have heard called "flow based programming", co-routines and inversion of control strategies (not just performance based approaches).

Also I'm interested in "failed" or, rather, currently unpopular approaches such as parallel-apply (Connection Machine Lisp ?????) and so on and so forth.

While not essential, it would be great to have examples explained in the context of what can be done in a strongly typed language.

Any and all pointers to such materials greatly appreciated.

Scott

Is anybody aware of a standard "toy" version of Scheme that is used for experimenting with Lisp-like languages? I'm thinking of something similar to MiniML's relationship with the ML family. I'm aware of Clinger's Core Scheme language, but this does not include macros, and I think they will be important for what we plan to do.

Of course, we could define our own language, but being able to point to a standard language will be much better.

I am a mathematics professor ^*. I was approached recently by one of our talented computer-science undergraduates at the university where I work, who is in her senior year and interested in taking a reading course in the applications of mathematical logic to computer science.

This undergraduate recently completed a summer project with the author of Twelf, formalising the ‘simplification’ SASyLF, and I get the impression that her interest is much more in the sorts of logic that arise in computer-assisted (mathematical) theorem proving than in the logic of programming per se—that is, I think that she's not particularly interested in temporal logic and other such proving-programs-correct stuff. She specifically mentioned wanting to understand the SLDNF logic behind Prolog, and I feel qualified to start there, but don't really know where to go next. I guess that I want to dig deeper into HM type inference (although she's already studied TAPL on her own, I believe), the calculus of inductive constructions, and that sort of thing—but these are mostly just (to me) buzzwords that I've picked up, and I'd like to put together some sort of coherent reading course. Suggestions?

^* To clarify, I'm mentioning this not to brag, but rather to give an idea of what a stretch this course will be for me. (I'm a representation theorist, not a logician.) Thus, don't hesitate to give references to things that “everybody knows”—almost assuredly, I don't!