Lambda the Ultimate

The famous three approaches to programming language semantics are axiomatic, operational and denotational semantics. The famous two approaches to logic semantics are proof theory and model theory.

I find denotational semantics similar to model theory, and operational semantics similar to proof theory. However, I find no analogue to axiomatic semantics, and I wonder if there is one, and if not, why?

In model theory, one takes an abstract logical language and defines its meaning within an existing theory: classical logic is interpreted in set theory (models are simple sets), intuitionistic logic in Kripke Scenarios (or Heyting Algebras), etc. In essence, we define the meaning of the new language in terms of existing, familiar languages. This is no other than denotational semantics, where our programs denote structures in existing, well-defined structures.

In proof theory, we associate no inner meaning with the language. Rather, the meaning emerges out of the symbol pushing that is the proofs. Operational semantics operates along the same lines, mechanically manipulating program text, and the meaning emerges out of the textual juggling. Moreover, many modern operational semantics are actually given as a proof system, the theorems being the valid executions of the language.

However, I do not recognise a similar analogy for axiomatic semantics. Am I missing something? Or is it simply because we do not want to explain one logic with another? Or perhaps the power of axiomatic semantics is the augmentation of the computable language with uncomputable/high complexity constructs, something that does not always interest logicians?

I am working on a rather simple object-oriented programming language. Here are some minor differences from a Java:

1. No downcasting (i.e. casting from a super-type to a sub-type [edit: thanks Ohad!])
2. A universal variant (i.e. can hold any value plus type information)
3. No virtual functions (dynamic dispatch through interfaces only)

What I am wondering about now (and I wrote a bit more on my blog) is whether preventing downcasting would cause any long term problems (in other words, has the community reached a consensus on this issues), and whether a variant type can cause violations of the Liskov substitution principle. Any insights into the problem, would be appreciated.