The tag has no wiki summary.

learn more… | top users | synonyms

0
votes
0answers
9 views

using ontology as a database model for reasoning on meta data

I'm working on a data warehouse design methodology starting from data sources model. This methodology requires the data sources conceptual model to captured by OWL ontology (only TBox). I need ...
3
votes
2answers
93 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 ...
4
votes
1answer
332 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
153 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
83 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
103 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 ...
2
votes
2answers
167 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 ...
8
votes
2answers
367 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
151 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
98 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
86 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
167 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 ...
3
votes
0answers
225 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
192 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
386 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
519 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 ...
1
vote
3answers
624 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 ...
4
votes
1answer
330 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 ...
7
votes
1answer
866 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
215 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 ...
5
votes
2answers
890 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
123 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
674 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
719 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 ...
7
votes
2answers
218 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
502 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
348 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: ...
7
votes
0answers
262 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
373 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 ...
15
votes
4answers
669 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 ...
12
votes
3answers
512 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 ...
27
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 ...
18
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
241 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
658 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
186 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
365 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 ...
19
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 ...
17
votes
4answers
1k 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
399 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 ...