Lambda the Ultimate

What is the relation between programming languages, model theory, and proof theory? I heard proof theory is more concerned with "syntax" whereas model theory is more concerned with "semantics". Would it be true to say that operational semantics corresponds to proof theory and denotational semantics to model theory? If yes, how exactly do they relate to each other?

By the way, a small related question: What exactly is a "theory" when someone says, he developed (say) a "Theory of Objects" like Abadi/Cardelli?

OpenSpice is an openly available specification of the Spice language - a modern programming language with some nice XML processing features. It is designed with the needs of part-time or occasional programmers in mind. The language features are properly separated and their corner cases have been eliminated. This design means that if you only use Spice occasionally, you're likely to find it easy to come back to despite the breaks.

The most similar well-known language is probably Common LISP together with CLOS. But Spice has a rich Algol-like external syntax, an XML transport form, and makes multiple values a key feature. The way Spice deals with multiple values is, we think, the feature that will strike most programmers as special.

I am not sure how interesting this really is, but the language seems to have some amusing features that you may want to explore.

This paper presents the design of a functional macroprogramming language for sensor networks, called Regiment. The essential data model in Regiment is based on region streams, which represent spatially distributed,time-varying collections of node state. A region stream might represent the set of sensor values across all nodes in an area or the aggregation of sensor values within that area. Regiment is a purely functional language, which gives the compiler considerable leeway in terms of realizing region stream operations across sensor nodes and exploiting redundancy within the network.

The operations on region streams include fold and map. The language uses monads to represent time varying values.

I know nothing about sensor networks (this paper is from DMSN 2004: the First Workshop on Data Management for Sensor Networks) so I can't judge how useful this project really is.

Notice that Regiment isn't implemented yet. Only a highly restricted (dynamically typed) subset is.