Lambda the Ultimate

Tim Harris, Simon Peyton-Jones. Transactional memory with data invariants. March 2006. TRANSACT '06, to appear.

This paper introduces a mechanism for asserting invariants that are maintained by a program that uses atomic memory transactions. The idea is simple: a programmer writes check E where E is an expression that should be preserved by every atomic update for the remainder of the program’s execution. We have extended STM Haskell to dynamically evaluate check statements atomically with the user’s updates: the result is that we can identify precisely which update is the first one to break an invariant.

The STM approach is sometimes described as being "like A and I" from ACID database transactions; that is, atomic blocks provide
atomicity and isolation, but do not deal explicitly with consistency or durability. This paper attempts to include “C” as well, by showing how to define dynamically-checked data invariants that must
hold when the system is in a consistent state.

While the basic idea is straightforward, the discussion of the design decisions in section 3.5-3.7 is an interesting exploration of the design space.

The implementation technique and operational semantics are the main contributions.

Previous draft discussed here.

Modeling Languages: Syntax, Semantics and all that Stuff (or, What's the Semantics of "Semantics"?)
by David Harel, Bernhard Rumpe

Motivated by the confusion surrounding the proper definition of complex modeling languages, especially the UML, we discuss the distinction between syntax and true semantics, and the nature and purpose of each.

This paper is rather light on greek letters (and category stuff is absent as well). Instead, it aims to introduce the notions of syntax, semantics, and formal definition of languages in plain prose.
If you never understood why bother with formal definitions - consider reading this!

You might want to read a longer version (Modeling Languages: Syntax, Semantics and All That Stuff Part I: The Basic Stuff). Unfortunately, I was unable to find parts II and III (The Advanced Stuff and The Really Hard Stuff) online.