Time

Time has passed quickly, and my posts have been infrequent of late. That's because I have been busy with a couple of things. Apologies all around.

First, I've been working on a method of implementing the dependently typed lambda calculus via compilation. Specifically, I've been looking at how to compile (or translate, if you like) Logical Framework specifications to lambdaProlog, a higher order logic programming language with at least one efficient compiled implementation (Teyjus, which I have worked on during my undergraduate and graduate studies; there are probably more).

Programming with LF is usually achieved by encoding judgments as dependent types and then searching for inhabitants of particular instances of these type families; I won't go into detail, but instead point you towards the excellent LF implementation Twelf, which does many things, including allow you to program in this way. My implementation is organized around compiling an LF specification to a lambdaProlog module, and then querying that module to find inhabitants of particular types.

Second, my friend and colleague David Baelde has recently begun a year long post-doc at the University of Minnesota (which is where I am), so we've been finding him a place to stay and what not, as well as working away (on, amongst other things, a proof that the translation I mention above is correct).

But, now things are settling a bit, and I should have time to write more about Mix -- I'll have to if I want to write a thesis proposal on the ideas I've been describing.