Uday Reddy
  • Member for 9 years, 11 months
  • Last seen more than a month ago
Use of Process Calculi and PL Theory for modern programming language development
1 votes

You say that "the true end goal would be to use the theory to actually build a PL." So, you presumably admit that there are other goals? From my point of view, the No. 1 purpose of theory is to ...

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
Is eta-equivalence for functions compatiable with Haskell's seq operation?
2 votes

I am not sure if the Haskell report defines the semantics rigorously enough to settle the question about what $\lambda x.\, \bot$ should mean. However, it is common experience in Haskell as well as ...

View answer
Difference between abstract machines and calculi
1 votes

I would add that, typically, one uses the term "calculus" when the evaluation rules are expressed at the level of the source language. One use the term "abstract machine" when addition "machine-level"...

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
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
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
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
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
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
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
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
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
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
Submitting other people's work to the arXiv
1 votes

I think this is tricky territory. The author of any creative work legally owns the copyright for that work unless he/she cedes it to another party. Notwithstanding the legal issues, any researcher ...

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
Regular languages from category-theoretical point of view
4 votes

Looking at the world using category theory goggles is called categorification. Sometimes it produces really nice and surprising results. Physicists have begun to say that thinking of a group as a ...

View answer
Unary parametricity vs. binary parametricity
4 votes

Let me a bit more abstract in answering this. At each arity $n$, you have the following situation: $n$-ary relations $R$ can be embedded into $(n+1)$-ary relations by defining $R'(\vec{x},y) \iff R(\...

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
Unary parametricity vs. binary parametricity
2 votes

Probably the easiest paper to read for the applications of binary parametricity is Wadler's Theorems for Free!. Actually, I am a bit surprised by the question because binary parametricity is what is ...

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
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
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
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
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 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
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
Where can I find an elementary small-step structural operational semantics for closures?
4 votes

Closures form an important concept that I try to teach in my undergraduate Programming Languages class. You can find my lecture notes online. The Handout 8 shows big step semantics using ...

View answer
Confusing (to me) statement from "Type Classes in Haskell"
4 votes

[This is the same answer as Andreas Rossberg's, a bit more elaborated.] Note that the only way you can overload a function symbol in Haskell is via type classes. So, if I want to define < for ...

View answer