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.9k
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 ...
3 votes
Accepted

Do realizable systems always have some non-well-founded sets?

You are using the wrong definition of well-foundedness. Let $R \subseteq A \times A$ be a relation. Consider the following definitions: $R$ is inductive when for all $B \subseteq A$, if $\forall x \...
Andrej Bauer's user avatar
  • 28.9k
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.9k
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
2 votes

Do realizable systems always have some non-well-founded sets?

CZF includes the $\in$-induction axiom, which is the constructively sensible version of the foundation axiom. So everything in one of its models is well-founded in that sense. However, while I'm no ...
Dan Doel's user avatar
  • 996

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