A Tail-Recursive Machine with Stack Inspection. John Clements and Matthias Felleisen, TOPLAS 2004.
This seems to be an introductory ("aimed specifically at non-theoreticians") set of articles on OO type theory. The author is Tony Simons and the articles were all published in the Journal of Object Technology.
The Rho-calculus is a calculus of pattern matching that embeds the lambda-calculus in a very simple manner, and also naturally accomodates a number of extensions of the lambda-calculus. It encodes the results of pattern matching in a manner that ensures confluence of the whole calculus.
It was proposed by Horatiu Cirstea and Claude Kirchner in 1998, and Matching Power, a 2001 RTA paper, is maybe the nicest introduction to the calculus. Kirchner's research group maintains a list of papers.
Postscript There was an LtU classic story on the rho-calculus as well...
Following the story on Mind Mappers and other RDF comments of late, I thought this NLP slide show (PDF) should get a story. Dr. Adrian Walker offers an interesting perspective in a friendly crayon-colored format, including a critique of RDF. Source site Internet Business Logic has other offerings including an online demo.
This is an excellent example of how the ML module language doesn't merely provide encapsulation but also strictly adds expressive power. It also demonstrates how a dynamic language (Lua) can be embedded in the statically-typed context of ML. Finally, it demonstrates that none of this need come at the expense of separate compilation or extensibility. Norman Ramsey's work is always highly recommended.
This might be interesting to folks curious about how to formalize a real language, or about how PLT Redex works in practice.
There's a neat thread about strong normalization happening on The Types Forum.
Termination is good:
Termination is good!
Termination is good and with fixpoints is turing complete?
Terminating reductions allows exhaustive applications of optimizations:
The problem: Most languages don't have formal specifications.
The solution (maybe): Make specification easier by using mechanized tools (for example, use Twelf).
The presentation: here (Robert Harper, ICFP'05).
The conclusion: You decide.
zfs-talk: Expanded talk with the demo. It was originally presented as an extra demo at the Haskell Workshop 2005
The Essence of Dataflow Programming
If you've ever wondered about dataflow or comonads, this paper is a good read. It begins with short reviews of monads, arrows, and comonads and includes an implementation. One feature that stood out is the idea of a higher-order dataflow language.
Active forum topics
New forum topics