11 votes

What are pertinent references to cite on Scott domains?

I asked Dana Scott who kindly responded. I am relaying his answer: I think the paper “A type-theoretical alternative to ISWIM, CUCH, OWHY” answers the questions and gives the context of the discovery....
Andrej Bauer's user avatar
  • 28.8k
7 votes

What are pertinent references to cite on Scott domains?

First papers Scott (1993), A type-theoretical alternative to ISWIM, CUCH, OWHY. This 1969 manuscript was later published in TCS. The title is a bit odd but it seems to hide the very first written ...
2 votes
Accepted

Denotational semantics of intersection types

Intersection types appear in typed programming languages to capture the idea that a given expression may carry multiple functionalities. For example, given a type $\mathsf{read}\;\alpha$ of readable ...
Andrej Bauer's user avatar
  • 28.8k
2 votes

Denotational semantics of intersection types

Later edit: When I wrote the answer below, I was thinking of intersection types as they are understood in the context of the untyped $\lambda$-calculus. It is now clear that this is not the right ...
Damiano Mazza's user avatar
1 vote
Accepted

What's the relation between applicative bisimulation and context equivalence in the $\lambda$-calculus?

It took me a while to realize, but, at least for the standard $\lambda$-calculus, those two should actually coincide. I'm not sure if there's any reference to this (I'd like to see it if there is!), ...
paulotorrens's user avatar
1 vote

A mathematical (categorical) description of type classes

Here is a categorical description of (certain kinds of) typeclasses. So far, I can fully elaborate this only for simpler typeclasses such as monoids or semigroups, not for type constructor typeclasses ...
winitzki's user avatar
  • 304

Only top scored, non community-wiki answers of a minimum length are eligible