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.
Unlike the previous approaches, the latest implementation is generic. Shift and control share all the same code, and differ in only one boolean flag. Therefore, it becomes possible to mix different control operators in the same program. Furthermore, the latest implementation is direct rather than emulation (in terms of an object-level shift), therefore, it has the best performance. The code is surprisingly simple, compared with the previous implementation of 'control' by Sitaram and Felleisen, and does not require equality on continuations. All four delimited control operations do indeed reduce to call/cc and one global mutable cell, and hence have a quite simple CPS transform. That has been known since the paper by Chung-chieh Shan (Scheme Workshop, 2004). The current code shows that result more directly.
Oleg's implementation provides all four Friedman-Felleisen delimited control operators: from -F- (similar to cupto) to +F- (aka control) to +F+ (aka shift). The R5RS Scheme code is parameterized by two boolean flags: is-shift and keep-delimiter-upon-effect. All four combinations of the two flags correspond to four delimited control operators.
Active forum topics
New forum topics