Lambda the Ultimate

OCaml Light: a formal semantics for a substantial subset of the Objective Caml language.

OCaml light is a formal semantics for a substantial subset of the Objective Caml language. It is written in Ott, and it comprises a small-step operational semantics and a syntactic, non-algorithmic type system. A type soundness theorem has been proved and mechanized using the HOL-4 proof assistant, thereby ensuring that the proof is free from errors. To ensure that the operational semantics accurately models Objective Caml, an executable version of the semantics has been created (and proved equivalent in HOL to the original, relational version) and tested on a number of small test cases.

Note that while we have tried to make the semantics accurate, we are not part of the OCaml development team - this is in no sense a normative specification of the implemented language.

From a team including Peter Sewell (Acute, HashCaml, Ott).

I continue to believe that things are heating up nicely in mechanized metatheory, which, in the multicore/multiprocessor world in which we now live, is extremely good news.

Hi,
I am studying lambda-calculus (untyped and typed). My teacher often uses the derivation trees.

For the untyped lambda calculus, such a tree has the following properties:

Starting from any lambda term T, we have:
(I use \ for lambda)
- if T=x, we build a terminal leaf node with label x

- if t=\x.M, we build a node with label \x with just one son, which is the subtree obtained applying the definition on M

- if T=(MN), we build a node with label @ with two sons. These are the subtrees obtained applying the definition on M and N.

This is not difficult, but I can't find examples of these trees on internet.

For the typed lambda calculus I can't really understand the method to check if a term is well typed or to assign a type to a term. I mean, using the tree system.

Do you know any good source where I can learn how these trees work?

Thanks,
Carlo

I am creating an interpreted game scripting language. Not having the theoretical background to help me develop and then implement a syntax, after a few attempts in that direction I decided to start from a register machine model, thinking that I would end up with something like a high-level assembler. Then, because my implementation language is haXe, which allows for dynamic types, I made a major change to the model:

There is no longer a separate space between program data and registers. Instead, thinking of how I can provide an infinite number of registers in my machine, I merged the ideas into one data structure. The first term that came to mind to describe this was "codeblock."

The codeblock contains both an integer opcode and data; the data is dynamic and can contain any haXe type. Passing data from one block to another is done at the source level, by making the relevant code all point to a third-party codeblock which has been agreed upon as a storage device. No specific ordering of codeblocks is dictated, but for practical convenience a "next" reference to a subsequent code block is also included for linear execution.

What I realized, as I built this system, was that the source code format was going to end up being tied to a customized editor which can deal with the data structures directly. At first I thought I would simply be mapping some of the higher level data structures in haXe to opcodes, and allowing the user to mark "variables" that get turned into codeblocks in a compilation step, but I gradually realized that with the editor's ability to browse, inspect, and link up references between codeblocks, there's a lot of potential power.

I added a stack for subroutine calls. Then, thinking a little more, I added a separate stack and a new referencing field in the codeblock for macros; as I envision it now, before executing the opcode of a codeblock, the interpreter looks to see if a macro codeblock is available. If it is, it jumps to that code and runs it first. The block that returns from a macro copies the contents of its data, which is itself another codeblock, to the caller. I don't have a lot of experience with constructs like this, though, so this may turn out to be wrongheaded.

This is all in very early stages. I've been sticking to writing stuff I can implement; my reference implementation to execute the above described is currently very small(under 200 lines) and surprisingly straightforward. I need to test it, work out the bugs, and start writing an editor. For the practical purposes I set out to achieve, I think I have something workable.

But my question is whether anyone knows of similar concepts to mine. It seems like any dynamic language could easily implement the same behavior, yet I know of nothing quite like this.