## User login## Navigation |
## Theory## Module Mania: A Type-Safe, Separately Compiled, Extensible InterpreterModule Mania: A Type-Safe, 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 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. By Paul Snively at 2005-12-07 14:58 | DSL | Functional | General | Implementation | Semantics | Theory | Type Theory | login or register to post comments | other blogs | 6378 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 2005-12-07 14:51 | General | Implementation | Semantics | Theory | Type Theory | login or register to post comments | other blogs | 5315 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
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 2005-11-17 12:31 | Implementation | Lambda Calculus | Theory | Type Theory | 15 comments | other blogs | 6521 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. ## Zipper-based file server/OS
zfs-talk: Expanded talk with the demo. It was originally presented as an extra demo at the Haskell Workshop 2005 By shapr at 2005-10-08 10:10 | Fun | Functional | Implementation | Theory | 21 comments | other blogs | 29314 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 higher-order dataflow language. By shapr at 2005-09-21 22:23 | Functional | Implementation | Logic/Declarative | Theory | 12 comments | other blogs | 19571 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 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. ## 'Information and Computation' Open Access
I found this in my mail.
Those of a more theoretical bent will find lots of interesting articles there. ## Trampolining Architectures
Trampolining Architectures
A trampolining architecture is a special case and extension of a monad which is useful in implementing multiprogramming. Five trampolining architectures, operating over the range of two trampolining translations, are presented. The effects of the architectures are cumulative. Some increase the breadth of multiprogramming facilities provided. Others demonstrate the potential for more efficient implementation. Finally, we demonstrate the applicability of trampolining to languages without closures.We discussed more than once Trampolined Style, but never this paper by the same authors (except Wand). Published one year later, it discusses more options, and more importantly, shows relations between trampolines and monads. If you are interested in design and implementation of PLs, and you never heard about tramplines - you should. ## Causal Nets
Causal Nets
The network approach to computation is more direct and "physical" than the one based on some specific computing devices (like Turing machines). However, the size of a usual -- e.g., Boolean -- network does not reflect the complexity of computing the corresponding function, since a small network may be very hard to find even if it exists. A history of the work of a particular computing device can be described as a network satisfying some restrictions. The size of this network reflects the complexity of the problem, but the restrictions are usually somewhat arbitrary and even awkward. Causal nets are restricted only by determinism (causality) and locality of interaction. Their geometrical characteristics do reflect computational complexities. And various imaginary computer devices are easy to express in their terms. The elementarity of this concept may help bringing geometrical and algebraic (and maybe even physical) methods into the theory of computations. This hope is supported by the grouptheoretical criterion given in this paper for computability from symmetrical initial configurations.The nets of this paper are different from belief nets or Bayesian nets, which are also known under name "causal nets". No doubt, modeling the history of computation rather than the current state is nothing new, but this paper tries to find new applications for that. |
## Browse archives## Active forum topics |

## Recent comments

1 hour 28 min ago

4 hours 22 min ago

7 hours 8 min ago

12 hours 15 min ago

15 hours 41 min ago

3 days 5 hours ago

3 days 7 hours ago

3 days 8 hours ago

3 days 9 hours ago

3 days 9 hours ago