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
8 votes
Accepted

The precise definition of Normalization By Evaluation?

The difference you see between higher-order and closure-based representations is a lot smaller than it first seems: the closure-based representation arises as the defunctionalisation of the higher-...
Neel Krishnaswami's user avatar
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 ...
7 votes
Accepted

Precise definition of syntatic categories / syntatic domains in abstract syntax

Most people avoid giving precise descriptions of what a syntactic category is, because if you do it properly with all the details, the ratio of insight to necessary mathematical sophistication ends up ...
Neel Krishnaswami's user avatar
5 votes
Accepted

Given a domain, how do we build a language whose denotation is the domain?

As it turns out, the OP is interested in the specific case of the interval domain. Martín Escardó's PhD thesis "PCF extended with real numbers: a domain-theoretic approach to higher-order exact ...
Andrej Bauer's user avatar
  • 28.9k
4 votes

Books on programming language semantics

I would like to add two books not found on the answers given up to now: Aaron Stump, Programming Language Foundations David Schmidt, Denotational Semantics: A Methodology for Language Development ...
Jay's user avatar
  • 982
4 votes

Is there a full abstraction result for an untyped lambda calculus?

Full abstraction means that denotational equality coincides with observational equivalence (under all contexts), but that notion depends on what observations you choose. If your observation on a term ...
Lê Thành Dũng 'Tito' Nguyễn's user avatar
4 votes

Precise definition of syntatic categories / syntatic domains in abstract syntax

I never found an explicit definition either, but I have inferred the folowing. As I understand, you split the language into syntactic domains; with the addition that syntactic domains must be fully ...
Jay's user avatar
  • 982
4 votes

Categorical semantics for non-monotonic logics?

[My apologies for writing this as an answer, despite the fact that it is basically just a comment to the previous answer. But I am not allowed to post a comment up there, since I do not have enough "...
Domenico Ruoppolo's user avatar
3 votes

Induction-recursion in models other than $\mathbf{Set}$

Define an IR system be a family $U \in \mathrm{Set}$ and a function $\phi \in U \to \mathrm{Set}$. IR systems form a domain. The least element is $\bot = (\emptyset, !)$. The order relationship $(U, \...
Neel Krishnaswami's user avatar
2 votes

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
  • 389
2 votes

Observational Equivalence of open terms in PCF

Got the answer, thanks to jonsterling on reddit for the insight. The error is that both M and N written as full judgements, ...
Adribar's user avatar
  • 31
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
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 possible error in the semantic chapter of the ISO standard for the Z specification notation

Firstly, in addition to the Standard from 2002, there is also Technical Corrigendum 1 (TC1) from 2007 which fixes a number of issues. I don't know of any combined document. Both documents are ...
Phil Clayton's user avatar

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