My impression is that, by and large, traditional algebra is rather too specific for use in Computer Science. So Computer Scientists either use weaker (and, hence, more general) structures, or ...

I have an answer to this question which is possibly novel. In fact, I am still thinking through it for the last 6 months or so, and it hasn't been written about in papers yet. The general thesis is ...

[I haven't thought deeply about the issues of object-oriented type systems, but I will say what I know to get the discussion going.] We say that $A$ is a subtype of $B$ if all $A$-typed values can be ...

Perhaps I can try giving a less metaphysical answer. There is a language, a logical language, that we are studying. In this language, there are things called "propositions" which are supposed to be ...

I would divide the books on programming language semantics into two classes: those that focus on modelling programming language concepts and those that focus on the foundational aspects of semantics. ...

I am happy with Adrej's answer, but I would like to drill down further. To start with, denotational semantics wants to say something like "the meaning of this notation is that". A real semanticist ...

Let us call a logic "symmetric" where a $-A$ ("not A") assumption means the same as proving $A$ and a proof of $-A$ means the same as an assumption of $A$. Classical logic and linear logic are ...

Indeed, there is a different notion than isomorphism which is more useful in programming. It is called "behavioural equivalence" (sometimes called "observational equivalence") and it is established ...

I am coming to this question late, but it is a fascinating question. So, here are my views. When I was an undergrad, we had a great Math professor, who used to give us lectures on history and ...

Unfortunately, there are too many things are going on here. So, it is easy to mix things up. The use of "full" in "full completeness" and "full abstraction" refer to completely different ideas of ...

The answer to your question is really there in Reynolds's fable (Section 1). Let me try and interpret it for you. In a language or formalism in which types are treated as abstractions, a type ...

[One more answer. It is probably uncool to pile up several answers. But, hey, this is a deep issue.] I said that I agreed with Andrej's answer, but it seems that I don't agree entirely. There is a ...

What proof system is being considered when discussing resolution? Is it just the resolution rule? What are the other rules? I discuss resolution in the context of "clauses", which are sequents made ...

Normal research papers are written primarily for other researchers, typically people in the same field, who are also at the cutting edge of research themselves. It is not surprising that they are ...

[Hopefully, this is my last answer to this question!] Ohad's original question was about how denotational semantics differs from structural operational semantics. He thought that both of them were ...

The answer is complicated, for two reasons. Different people in Computer Science interpret the term "object" differently. One is that an object consists of some data and operations packaged ...

A lot of the senior Computer Scientists in Britain have had industrial experience before they came to work in academics. Christopher Strachey, the founder of denotational semantics, was a consultant ...

I don't have a specific recommendation for your reading list, but I want to alert you to the excellent survey on "Rewrite Systems" by Dershowitz and Jouannaud in Handbook of Theoretical Computer ...

This additional response is to amplify the point that denotational semantic models are designed to "explain" computational phenomena. I will give a series of examples from the semantics of imperative ...

Unfortunately, the remark of Wadler is too cryptic for me to tell what use he wanted to make of "lax natural transformations". Here is a guess. Relation-preservation squares can often be recast as ...

Are there any good reasons why PL theorists prefer naturals instead of integers? There are some, but in a text book on programming language semantics, I think there is no technical reason why they ...

(Gosh, Neel, that was a tough question.) The "folk model" of linear logic is definitely the coherent spaces model, discussed in Girard's Linear Logic paper (and also in "Proofs and Types"). This is ...

The second paragraph of Plotkin's 1973 Memo on Lambda-definability and Logical Relations says this: "The definition of logical [relation] is derived from a corresponding one of M. Gordon for the ...

The standard presentation of program transformation ideas is unsound, quite unfortunately. They usually think of program transformation as forward deduction. Using equational reasoning, you can ...

I would expect that the empty relation corresponds to the always-zero probability distribution. Disjoint union corresponds to addition of probability distributions. However, standard union would be ...

In addition to Andreas's excellent answer, please keep in mind that type classes are meant to streamline overloading, which affects the global name space. There is no overloading in Haskell other ...

There are unfortunate confusions in the way you have posed the question. Programs have semantics. Programming Languages are given semantic definitions. In more detail: every program has a meaning, ...

Legally speaking, the term "calculus" is almost always used to describe a language, i.e., a piece of syntax, with added rules of calculation or reasoning. Examples include the good old predicate ...

Indeed there is a Wikipedia entry on metaprogramming. The question "What are staged functions?" on cs.stackexchange is also relevant.

If you enlarge the idea of "programs" to include Turing machines, then the original Turing's description of their semantics was as transition systems. So, I think transition systems have always been ...