The tag has no wiki summary.

learn more… | top users | synonyms

-2
votes
0answers
40 views

Small-step semantics: for-loop

I'm trying to construct the small-step semantic rules involving the for-loops, but I can't find anything about it in the literature (only about while-loops). I was wondering if anyone could help me ...
6
votes
0answers
62 views

Equivalence of categories of directed complete posets

I asked this question there: http://math.stackexchange.com/questions/700975/equivalence-of-categories-of-directed-complete-posets. Since I had no answer, I try here. In the book ``Domains and ...
8
votes
2answers
296 views

Full Completeness vs Full Abstraction of a program translation

Compiler verification efforts often come down to proving the compiler fully abstract: that it preserves and reflects (contextual) equivalences. Instead of providing full abstraction proofs, some ...
6
votes
0answers
178 views

Types as theories

I am studying Goguen's paper Types as theories [1]. Based on Goguen's paper, are the following true? Subsort inheritance provides a classification of values, every value of the sub-sort is a value ...
0
votes
2answers
223 views

Meaning of program as solution of a recursive equation

I would like to ask you a question about (denotational?) semantic of program. After defining program as a transition system, and the semantics as a transition function: $$next: States \rightarrow ...
0
votes
0answers
65 views

Semantics of a programming language [duplicate]

A newbie question, if I may... Could you be so kind and explain to me in plain english meaning of 'denotational semantics' and 'operational semantics'? I'm familiar with the definitions and have read ...
11
votes
1answer
468 views

Can Scheme's call/cc implement all known control flow structures?

The page "Advanced Scheme: Some Naughty Bits" states: Continuations are a powerful control-flow construct from which nearly any other control-flow structure [...] may be derived. I thought ...
6
votes
1answer
683 views

What is the difference between meaning and denotation?

In programming language semantics, it is often heard that people talking about meaning and denotation. They seem not to be the same. What is the difference? Is the former associated with ...
10
votes
1answer
425 views

A mathematical (categorical) description of type classes

A functional language can be viewed as a category where its objects are types and morphisms functions between them. How do type classes fit in this model? I assume we should only consider those ...
8
votes
1answer
179 views

Uses of quasi-PERs/difunctional relations/zig-zag relations?

Given sets $A$ and $B$, a difunctional relation $(\sim) \subseteq A \times B$ between them is defined to be a relation satisfying the following property: If $a \sim b$ and $a' \sim b'$ and $a \sim ...
9
votes
1answer
144 views

Reference for the undefinability of modulus of continuity functional in PCF?

Can someone point me to the reference for the non-definability of the modulus of continuity functional in PCF? $\newcommand{\N}{\mathbb{N}}$ $\newcommand{\bool}{\mathsf{bool}}$ Andrej Bauer has ...
9
votes
1answer
309 views

Reasoning about non-deterministically terminating loops

Here's a "track B" question if there ever was one. Summary: the first thing I think of when I try to give a semantics to non-deterministic programs results in a semantics where I can't prove things ...
15
votes
2answers
504 views

What is the origin of logical relations?

I actually have two questions: Who first used logical relations to relate semantics? I traced them back to Reynold's "On the Relation Between Direct and Continuation Semantics", but I can't claim ...
6
votes
1answer
190 views

Has anyone studied “polynomially compact” metric spaces?

A subspace $S$ of a metric space $A$ is compact if it is complete and totally bounded. Here, complete means that every Cauchy sequence in $S$ has a limit also in $S$. For $S$ to be totally bounded, ...
14
votes
1answer
462 views

Fixed point theorems for constructive metric spaces?

Banach's fixed point theorem says that if we have a nonempty complete metric space $A$, then any uniformly contractive function $f : A \to A$ it has a unique fixed point $\mu(f)$. However, the proof ...
10
votes
1answer
254 views

Is Escardó's metric semantic for PCF+timeouts fully abstract ?

In his 1999 workshop paper "A Metric Model of PCF", Martín Escardó showed that it is possible to give a simple interpretation of PCF in the category of complete ultrametric spaces and ...
26
votes
7answers
2k views

What constitutes denotational semantics?

On a different thread, Andrej Bauer defined denotational semantics as: the meaning of a program is a function of the meanings of its parts. What bothers me about this definition is that it ...
13
votes
5answers
3k views

Books on programming language semantics

I've been reading Nielson & Nielson's "Semantics with Applications", and I really like the subject. I'd like to have one more book on programming language semantics -- but I really can get only ...
6
votes
1answer
238 views

In domain theory, what can the extra structure present in metric spaces be used for?

Smyth's chapter in the handbook of logic in computer science and other references describe how metric spaces can be used as domains. I do understand that complete metric spaces give unique fixed ...
8
votes
3answers
641 views

What is a good Category Theory-Domain Theory dictionary?

When dealing with the domain theoretic categories (say CPO and $\omega$CPO), I frequently wish for a dictionary for the language of category theory in domain theory. That is, given a concept, say ...
22
votes
2answers
750 views

What is the folk model of linear logic?

Probably the most common application of linear types in PL is to use them to give languages which control aliasing (i.e., a linear value has a single pointer to it, more or less). But there's a ...
12
votes
0answers
182 views

Generalizing limit-colimit coincidence to Scott-continuous adjunctions: any uses?

In Abramsky and Jung's 1994 handbook chapter on denotational semantics, after proving that the limit and colimit of expanding sequences exist and coincide, they have the following to say about ...