Uday Reddy
  • Member for 9 years, 11 months
  • Last seen more than a month ago
Uses of algebraic structures in theoretical computer science
Accepted answer
53 votes

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 ...

View answer
What are the differences between logical relations and simulations?
21 votes

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 ...

View answer
How does inheritance differ from subtyping?
Accepted answer
19 votes

[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 ...

View answer
What is the difference between propositions and judgments?
18 votes

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 ...

View answer
Books on programming language semantics
17 votes

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. ...

View answer
What constitutes denotational semantics?
16 votes

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 ...

View answer
How should I think about proof nets?
15 votes

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 ...

View answer
Data Structure isomorphisms
15 votes

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 ...

View answer
What is the theoretical basis of imperative programming?
14 votes

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 ...

View answer
Full Completeness vs Full Abstraction of a program translation
Accepted answer
12 votes

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 ...

View answer
How can relational parametricity be motivated?
12 votes

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 ...

View answer
What constitutes denotational semantics?
12 votes

[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 ...

View answer
Is propositional resolution a complete proof system?
Accepted answer
10 votes

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 ...

View answer
Are research papers hard to read?
10 votes

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 ...

View answer
What constitutes denotational semantics?
10 votes

[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 ...

View answer
Formal Definition/counter part in mathematics for “Objects” of Object Oriented Models
Accepted answer
9 votes

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 ...

View answer
Can one return to a TCS research job after an excursion to a non-research industry job?
9 votes

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 ...

View answer
Reading list on rewriting systems?
Accepted answer
9 votes

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 ...

View answer
What constitutes denotational semantics?
9 votes

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 ...

View answer
Natural Transformations and Parametricity
Accepted answer
8 votes

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 ...

View answer
Why naturals instead of integers?
7 votes

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 ...

View answer
What is the folk model of linear logic?
7 votes

(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 ...

View answer
What is the origin of logical relations?
Accepted answer
6 votes

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 ...

View answer
Preserving termination when rewriting recursive programs
Accepted answer
6 votes

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 ...

View answer
Is analogy between database and probability concepts legitimate?
6 votes

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 ...

View answer
Type classes vs object interfaces
6 votes

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 ...

View answer
How to define the formal and informal semantics of an algorithm as accurately as possible?
5 votes

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, ...

View answer
Semantics of concurrent languages
5 votes

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 ...

View answer
Newbie question: Meta-functions?
Accepted answer
4 votes

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

View answer
Early References for Transition System Semantics of Programs
4 votes

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 ...

View answer