Lambda the Ultimate

Logfun is a library of logic functors. A logic functor is a function that can be applied to zero, one or several logics so as to produce a new logic as a combination of argument logics. Each argument logic can itself be built by combination of logic functors. The signature of a logic is made of a parser and a printer of formulas, logical operations such as a theorem prover for entailment between formulas, and more specific operations required by Logical Information Systems (LIS). Logic functors can be concrete domains like integers, strings, or algebraic combinators like product or sum of logics.

Logic functors are coded as Objective Caml modules. A logic semantics is associated to each of these logic functors. This enables to define properties of logics like the consistency and completeness of the entailment prover, and to prove under which conditions a generated entailement prover satisfies these properties given the properties of argument logics.

Logic Functors form a framework for specifying new logics, and deriving automatically theorem provers and consistency/completeness diagnoses. Atomic functors are logics for manipulating symbols and concrete domains, while other functors are logic transformers that may add connectives or recursive structures, or may alter the semantics of a logic. The semantic structure of the framework is model theoretic as opposed to the verifunctional style often used in classical logic. This comes close to the semantics of description logics, and we show indeed that the logic ALC can be rebuilt using logic functors. This offers the immediate advantage that variants of ALC can be explored and implemented almost for free.

The use of OCaml functors here may be interesting even for those who aren't into logic languages. The system allows new logics to be created in OCaml itself, by simply composing OCaml functors. This is covered further in Implementation as ML Functors. The quickest way to get a feel for what this system does is to look at the examples.

Flapjax s a functional reactive compiler and Javascript library for creating interactive web GUIs, created by Brown PLT. You can try the compiler online, or read the docs to get more of an idea of how the language works. If you've used OO style MVC before, but not functional reactive programming (FRP), take a look at Flapjax for a different, and in my opinion, cleaner approach to the same problem.

If you're familiar with FrTime you'll recognise the elements of Flapjax -- Flapjax is essentially a Javascript implementation of FrTime, and a compiler from the Flapjax language to Javascript to make writing code less verbose. The key differences compared to the Haskell FRP tradition are that FrTime is asynchronous and uses mutable state. This means behaviours (time varying values) can be sampled at any time, whereas in Haskell FRP behaviours are all sampled at the same time, and it isn't necessary to use the arrow combinators to hide accumulators. Of course it isn't all roses: the implementation is more complex, and doesn't work well in, say, a continuation based web server as mutable state will mess up resumptions of previous continuations. (Don't get the idea that this is a problem for Flapjax -- it runs on the client, not the server.)

Here's something a little unusual... a novel.

A Madman Dreams of Turing Machines. Janna Levin.

In this remarkable work of fiction, astrophysicist Janna Levin reimagines the lives of two of the most important and influential minds of our time.

The narrator is a scientist herself, a physicist obsessed with Kurt Gödel, the greatest logician of many centuries, and with Alan Turing, the extraordinary mathematician, breaker of the Enigma Code during World War II.

The potential interest to this audience should be fairly obvious, although the book is centered at least as much on their substantial personal struggles as on their work. Here is the New York Times review, perhaps it would be nice to have an LtU review as well...