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-...
- 32.4k
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 ...
- 32.4k
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 ...
- 28.3k
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
...
- 982
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 ...
- 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 "...
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, ...
- 31
2
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, \...
- 32.4k
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!), ...
- 377
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 ...
- 29
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 ...
- 244
Only top scored, non community-wiki answers of a minimum length are eligible