User loginNavigation 
TheoryThe Theory of Classification  A Course on OO Type SystemsThis seems to be an introductory ("aimed specifically at nontheoreticians") set of articles on OO type theory. The author is Tony Simons and the articles were all published in the Journal of Object Technology.
If I've made a mistake above, try A Simons's bibliography or here. By andrew cooke at 20060228 23:22  OOP  Teaching & Learning  Theory  Type Theory  7 comments  other blogs  30941 reads
Rho calculusThe Rhocalculus is a calculus of pattern matching that embeds the lambdacalculus in a very simple manner, and also naturally accomodates a number of extensions of the lambdacalculus. 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 rhocalculus as well... Semantic Distance: NLP Not a Resource SinkFollowing 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 crayoncolored format, including a critique of RDF. Source site Internet Business Logic has other offerings including an online demo. By Mark Evans at 20060122 06:58  DSL  MetaProgramming  Semantics  Theory  XML  4 comments  other blogs  11344 reads
Module Mania: A TypeSafe, Separately Compiled, Extensible InterpreterModule Mania: A TypeSafe, Separately Compiled, Extensible Interpreter
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 staticallytyped 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. By Paul Snively at 20051207 14:58  DSL  Functional  General  Implementation  Semantics  Theory  Type Theory  login or register to post comments  other blogs  6606 reads
ClassicJava in PLT Redex
This might be interesting to folks curious about how to formalize a real language, or about how PLT Redex works in practice. By Paul Snively at 20051207 14:51  General  Implementation  Semantics  Theory  Type Theory  login or register to post comments  other blogs  5490 reads
What good is Strong Normalization in Programming Languages?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:
Rene Vestergaard also gave a link to a 2004 discussion of strong normalization on the rewriting list. By shapr at 20051117 12:31  Implementation  Lambda Calculus  Theory  Type Theory  15 comments  other blogs  6941 reads
Mechanizing Language Definitions
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. Zipperbased file server/OS
zfstalk: Expanded talk with the demo. It was originally presented as an extra demo at the Haskell Workshop 2005 By shapr at 20051008 10:10  Fun  Functional  Implementation  Theory  21 comments  other blogs  30814 reads
The essence of Dataflow Programming by Tarmo Uustalu and Varmo VeneThe 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 higherorder dataflow language. By shapr at 20050921 22:23  Functional  Implementation  Logic/Declarative  Theory  12 comments  other blogs  20970 reads
Generic implementation of all four *F* operators: from control0 to shiftUnlike 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 objectlevel 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 Chungchieh Shan (Scheme Workshop, 2004). The current code shows that result more directly. Oleg's implementation provides all four FriedmanFelleisen 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: isshift and keepdelimiteruponeffect. All four combinations of the two flags correspond to four delimited control operators. 
Browse archivesActive forum topics
New forum topics

Recent comments
20 hours 4 min ago
1 day 44 min ago
1 day 9 hours ago
1 day 18 hours ago
2 days 1 hour ago
2 days 20 hours ago
4 days 3 hours ago
4 days 13 hours ago
4 days 23 hours ago
5 days 2 hours ago