User loginNavigation 
SemanticsModule 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  7015 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  5742 reads
In the beginning was game semantics
In the beginning was game semantics
Giorgi Japaridze [...] the story and philosophy of computability logic (CL) [...]I already posted links to papers of Giorgi Japaridze several times, but most of them were pretty technical, and also that was before the latest expansion of LtU's readership. In short, CL is about trying to generalize traditional (both classical and intuitionistic) logic beyond batch computation (well, I hope everybody knows why logic is relevant to computation, if not  look for CurryHoward isomorphism, or CHI). There are several approaches to doing that, but Giorgi believes they go the wrong way by trying to build upon the syntax, while it's semantics that is primary. If you believe that computation is more than calculating a function, and that logic is a good way to understand computation  then I recommend to read at least the introduction and the references' list of this paper (the paper is a single chapter for a book, would love to see the whole book). Combining computational effectsWhile some researchers seek to generalize monads (to arrows), others try to narrow the focus to achieve a richer theory (and probably deeper understanding). Combining computational effects: commutativity and sum We begin to develop a unified account of modularity for computational effects. We use the notion of enriched Lawvere theory, together with its relationship with strong monads, to reformulate Moggi's paradigm for modelling computational effects; we emphasise the importance here of the operations that induce computational effects. Effects qua theories are then combined by appropriate bifunctors (on the category of theories). We give a theory of the commutative combination of effects, which in particular yields Moggi's sideeffects monad transformer (an application is the combination of sideeffects with nondeterminism). And we give a theory for the sum of computational effects, which in particular yields Moggi's exceptions monad transformer (an application is the combination of exceptions with other effects).A longer version: Combining Effects: Sum and Tensor By Andris Birkmanis at 20051005 14:31  Category Theory  Semantics  3 comments  other blogs  11301 reads
An Operational Semantics for R5RS Scheme
Jacob Matthews
and
Robby Findler bring us
An Operational Semantics for R5RS Scheme
(also available in PostScript):
This looks like excellent work, as we've come to expect from the PLT folk. The PLT Redex tool was previously discussed on LtU. If you're interested in checking it out, this page provides links to "everything you need to run PLT Redex and executable versions of every reduction system in the paper". To be presented at the 2005 Workshop on Scheme and Functional Programming, Tallinn, Estonia, 24 September, 2005.Thanks to Jens Axel SÃ¸gaard for bringing this paper to my attention. By Anton van Straaten at 20050914 17:47  Semantics  login or register to post comments  other blogs  42683 reads
A Typed, Compositional Logic for a StackBased Abstract Machine
A Typed, Compositional Logic for a StackBased Abstract Machine. Nick Benton. MSRTR200584. June 2005.
We define a compositional program logic in the style of Floyd and Hoare for a simple, typed, stackbased abstract machine with unstructured control flow, global variables and mutually recursive procedure calls. Notable features of the logic include a careful treatment of auxiliary variables and quantification and the use of substructural typing to permit local, modular reasoning about program fragments. Semantic soundness is established using an interpretation of types and assertions defined by orthogonality with respect to sets of contexts. By Ehud Lamm at 20050702 09:14  Implementation  Semantics  Type Theory  2 comments  other blogs  7411 reads
Revisiting coroutines
Taking into account real or imaginary interest to control operators on LtU, I believe this paper makes nice reading. See also Coroutines in Lua. By Andris Birkmanis at 20050627 16:56  Parallel/Distributed  Semantics  2 comments  other blogs  6141 reads
A Monadic Framework for SubcontinuationsA Monadic Framework for Subcontinuations
XQuery 1.0 and XPath 2.0 Formal Semantics  Last Call
(via Michael Rys)
This is a Last Call Working Draft. Comments on this document are due no later than 15 July 2005... I guess that those interested in this area know about this, and for others it is a bit too late to get involved, but at least it's good to know the status of the formal specification. On Evaluation Contexts, Continuations, and the Rest of Computation
Although already mentioned before, I believe this paper (which reconciles two approaches to defining continuations) deserves a separate story.
On Evaluation Contexts, Continuations, and the Rest of Computation Continuations are variously understood as representations of the current evaluation context and as representations of the rest of the computation, but these understandings contradict each other: plugging an expression in a context yields a new expression whereas sending an intermediate result to a continuation yields the final answer. We show that continuationsasevaluationcontexts are the defunctionalized representation of the continuation of a singlestep reduction function and that continuationsastherestofthecomputation are the continuation of an evaluation function. Furthermore, we show that defunctionalizing the continuation of an evaluator gives rise to the same evaluation contexts as in the singlestep reducer. The only difference is how these evaluation contexts are interpreted: a â€˜plugâ€™ interpretation yields onestep reduction, whereas a â€˜refocusâ€™ interpretation yields evaluation. By Andris Birkmanis at 20050608 13:45  Lambda Calculus  Semantics  1 comment  other blogs  4914 reads

Browse archivesActive forum topics 
Recent comments
6 days 4 hours ago
1 week 1 day ago
1 week 1 day ago
1 week 1 day ago
1 week 1 day ago
1 week 1 day ago
1 week 1 day ago
1 week 1 day ago
1 week 1 day ago
1 week 1 day ago