The tag has no usage guidance.

learn more… | top users | synonyms

6
votes
1answer
221 views

Standard reference for basic model theory definitions

I am trying to give a formal presentation of the model-theoretical semantics of a language and I am a bit lost in the terminology. In particular, could somebody clarify the exact definitions of model-...
0
votes
1answer
59 views

Observational Equivalence of open terms in PCF

The notion of observational equivalence is rather intuitive, but formally I'm having some doubts in the particular case of open terms. Lets consider the simple case where the terms ...
3
votes
1answer
92 views

In what fields does a knowledge of formal semantics prove useful?

(If this is better for programmers SE, let me know, but I imagined you guys would have more thorough answers) I'm a mathematics major, but I have a pretty deep interest in CS (especially in compiler ...
8
votes
2answers
207 views

Precise definition of syntatic categories / syntatic domains in abstract syntax

I have read the introductory parts of a couple of books on programming language semantics (Gordon, Winskel, Nielson & Nielson, Allison, Stump, Schmidt), and while I do understand what they mean by ...
0
votes
1answer
63 views

How to specify and verify Horn clauses (logic programming programs)? Semantics of Horn clauses

There are lot of applications of Horn clauses (notable examples include use of rules in cognitive architectures and knowledge bases, as well as use of rules in business rules programs). Are there ...
7
votes
2answers
183 views

What's the difference between reduction strategies and evaluation strategies?

From the evaluation strategy article on Wikipedia: The notion of reduction strategy in lambda calculus is similar but distinct. From the reduction strategy article on Wikipedia: It is ...
0
votes
0answers
141 views

How do we contribute to the lexicon of computer science?

What's the best way to contribute to the lexicon of computer science? There is an obvious organic nature to the naming of things in most sciences. The name of the discoverer is inherited or bestowed, ...
1
vote
1answer
61 views

What is the relation/difference between axiomatic and denotational semantics one one side, and the data flow analysis(DFA) on the other sied?

I am supposed to write a small paper about DFA in OOP for a CS class in theory. But I am required to connect that (DFA) to axiomatic and denotational semantics! I read few resources about axiomatic/...
1
vote
1answer
154 views

Name a set of program variables

I am interested in the set of the variables that satisfy the following properties. I would like to find a proper name for them. We assume that a program $\phi$ has a set of variables $v_0, \ldots, ...
5
votes
1answer
138 views

Categorical semantics for non-monotonic logics?

Are there any categorical semantics for non-monotonic logics? It appears that the simple answer to this is "No" since the obvious notion of composition fails for any model of a non-monotonic logic. ...
3
votes
2answers
162 views

What requirements should a denotational semantics for a programming language satisfy to be correct?

We have a programming language and its denotational semantic, like Tony Hoare's CSP with its syntax and denotational semantic e.g. stable failure and UTP. We want to extend the language (its ...
5
votes
1answer
671 views

How can I prove formally semantic equivalence of programming languages?

I would like to compare two languages which are from different programming paradigms. Both langauges are object oriented languages, but one of them a multiparadigm language because it supports ...
9
votes
1answer
163 views

Program Minimization

Circuit Minimization is the problem to minimize the size of a given circuit. Is there anything similar for general programs? In particular my question is - Do there exist algorithms to minimize the ...
1
vote
2answers
152 views

Tool for specifying operational semantics for given formally specified programming language

I am trying to translate code from one programming language into another (to be specific - from RuleML to Drools, but other pairs can be expected as well) and it would be nice to know - whether there ...
9
votes
1answer
208 views

What exactly does “semantically observable” side-effect mean?

I have question regarding pure functions. According to the Wikipedia page one of the requisites for a pure function is : Evaluation of the result does not cause any semantically observable side ...
3
votes
2answers
217 views

Difference between abstract machines and calculi

So, first of all: I'm not sure how to tag this question. Feel free to tag it differently. I recently started reading up on CHAMs, which can express different process calculi. Slightly confused, I go ...
12
votes
2answers
872 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 ...
4
votes
0answers
212 views

What's the connection between these two categories of games and innocent strategies?

Lately I've been reading a lot about game semantics and in particular the problem of PCF's full abstraction. I'm trying to understand how the definition from this article relates to the one found in ...
0
votes
1answer
117 views

How would you define a set of 'fundamental operations' over an object? [closed]

I'm writing an implementation for a common array structure. As you would find already familiar, an array is an ordered data structure that you can transform with different (hopefully self-explained) ...
1
vote
1answer
96 views

Is there good open source project that apply semantic web, modal logics, and similar technologies

Recently such themes as semantic web, modal logics, business rules have seen increased interest as research topics in computer science (alhough many of then have more than 80 years of history), but ...
5
votes
0answers
191 views

Is there a Galois correspondence between a Haskell class hierarchy and its instance hierarchy?

Can we consider a Haskell class as a loose signature-only-specification (denoting a theory) and an instance as an implementation (denoting a model)? In the example below the specification of the class ...
3
votes
0answers
260 views

Is there a model theory for Haskell type classes?

I am trying to understand the semantics of Haskell’s type classes (TCs) from a model-theory point of view. It might difficult to give precise model theoretic semantics to type classes (see 1, and 2). ...
6
votes
0answers
214 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 ...
5
votes
2answers
524 views

Formal representation of algorithm using recursive algebraic data types

I have an algorithm written in Haskell which I am describing in my thesis. In the code for the algorithm I have a recursive data type similar to this: data Data = A Int | B Data | C Data Now I ...
6
votes
2answers
741 views

Certified compiler and optimizations in Coq/Agda

I am interested in verified compilers formalized in Martin-Löf type theory, i.e. Coq/Agda. At the moment I’ve written a small toy example. Therewith I can prove that my optimizations are correct. For ...
2
votes
3answers
1k views

How to define the formal and informal semantics of an algorithm as accurately as possible?

I am currently researching ways to define the semantics of programs for some ideas I have for a new programming language. Most ways to define semantics involve mapping the programming language syntax ...
6
votes
1answer
363 views

Semantics of concurrent languages

I've seen that the preferred way to specify the semantics of a concurrent language is to use a process calculus (e.g. pi calculus, join calculus). But in the paper presenting the F# asynchronous ...
9
votes
1answer
2k 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 ...
7
votes
4answers
233 views

Early References for Transition System Semantics of Programs

I am trying to trace back the origins of transition system semantics for imperative programs. I am assuming a transition system is a tuple $(\mathit{States}, \mathit{Trans})$ consisting of a set of ...
8
votes
2answers
1k views

Formal Definition/counter part in mathematics for “Objects” of Object Oriented Models

This is a question I asked in mathematics SE forum, and I was referred here. So here is the question- I'm a newbie in both formal mathematics and theoretical computer science, so please bear with me ...
0
votes
1answer
131 views

Logic programming with integer or even floating point domains

I am reading a lot about logic programming - ASP (Answer Set Programming) is one example or this. They (logic programs) are usually in the form: [Program 1] Rule1: a <- a1, a2, ..., not am, am+1; ...
19
votes
5answers
747 views

Compiler correctness proofs

I am looking for tutorial material that covers compiler correctness proofs, preferably using denotational methods, at the level of a beginning grad student. Alternatively, do you know of some ...
15
votes
3answers
757 views

When can we say that two programs are different?

Q1. When can we say that two programs (written in some programming language like C++) are different? The first extreme is to say that two programs are equivalent iff they are identical. The other ...
8
votes
2answers
232 views

Where can I find an elementary small-step structural operational semantics for closures?

Lexical closures are an implementation technique in languages with first-class functions. I'm interested in a simple operational description of function closures. Does anyone know of such a ...
2
votes
2answers
696 views

Equivalence of two basic blocks

My questions: What are other names for this and similar problems and their fields? ("equivalence of varieties in universal algebra", "equivalence of algebraic structures", "rewriting systems for ...
13
votes
2answers
377 views

What are the equational laws for zero types?

Disclaimer: while I care about type theory, I don't consider myself an expert on type theory. In the simply typed lambda calculus, the zero type has no constructors and a unique eliminator: $$\frac{\...
7
votes
0answers
295 views

The semantics of Parsing Expression Grammars

Is there a simple and intuitive explanation for the fact that the following parsing expression (where S is the starting symbol, $...
16
votes
3answers
441 views

Is there any programming language theory describing foreign function interfaces (FFI) and multiple language bindings?

Is there any programming language theory describing foreign function interfaces (FFI) and multiple language bindings? I have asked some implementation issues on stackoverflow, which is not suitable ...
16
votes
4answers
782 views

How are imperative languages more different from each other than functional languages?

I'm reading Simon Peyton Jones's The Implementation of Functional Programming Languages and there's one statement that surprised me a little bit (on page 39): To a much greater extent than is the ...
13
votes
3answers
642 views

Formal Semantics of Programming Languages

I'm new to programming languages theory and I'm seeking for a good resource on a resource for formal semantics of programming languages. Specifically looking for structural operational semantics. I ...
33
votes
7answers
3k 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 doesn'...
24
votes
7answers
5k 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 ...
9
votes
1answer
292 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 ...
10
votes
3answers
753 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 ...
12
votes
0answers
207 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 ...
4
votes
3answers
371 views

Semantic distance between excerpts of text.

I'm wondering how far along the natural language processing is in determining the semantic distance between two excerpts of text. For instance, consider the following phrases Early this morning I ...
21
votes
4answers
1k views

Why do we need formal semantics for predicate logic?

Consider this question solved. I will not pick a best answer as all of them have contributed to my understanding of the topic. Im unsure what benefit we have by formally defining the semantics of ...
18
votes
4answers
2k views

How are side effects handled in semantics?

In Anthony Aaby's "Introduction to Programming Languages" section on Semantics, he makes the following observation: Much of the work in the semantics of programming languages is motivated by ...
4
votes
3answers
415 views

What applications of Cantor space are there?

Are there well-established applications of the Cantor space ($2^\omega$) in computer science, other than those connected with computable real arithmetic? John Tucker's page Computation on Topological ...