Programming languages, in particular, focussing on their semantics.

learn more… | top users | synonyms (2)

0
votes
0answers
25 views

SLR(1) vs LALR(1) when we use SLR(1) Grammar

i'm so glad that ask my first question on my favorite site. Infact i ran into multiple choice question in recent exam on Compiler Course. Suppose T1, T2 is created with SLR(1) and LALR(1) for ...
7
votes
2answers
153 views

What are some good introductory books on type theory?

I'm recently studying Haskell and programming languages. Could someone recommend some books on type theory?
6
votes
1answer
246 views

Describing state machines mathematically

The short paper "Computer Science and State Machines" by Leslie Lamport seems quite strange to me. On the one hand, I am surprised to see that an important hardware protocol called "two-phase ...
5
votes
1answer
160 views

Type theory for memory safe data structures

Data structures such as a doubly linked list and a B+ tree have blocks of memory that have multiple pointers to it. This creates the risk that a bug will allow memory to be accessed after being freed. ...
3
votes
2answers
87 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 ...
3
votes
0answers
106 views

Generalizing Haskell: could we replace Hask with Cat?

N.B. I asked the same question on Stack Overflow but it was suggested that it is too theoretical for this forum. It is great that Haskell allows us to walk around in the category $Hask$. But ...
4
votes
1answer
395 views

Is this behavior in a programming language inconsistent?

I'm developing a tiny programming language to try to wrap my head around type inference, and I'm trying to figure out if its behavior makes sense or not. Here's the problem: The identity function ...
6
votes
0answers
51 views

Hypersequents: proof term assigments or translations to hybrid logic

I've been looking at a modal logic with the axiom $$ (\Diamond A \land \Diamond B) \to \Diamond((A \land \Diamond B) \vee (A \land B) \vee (A \land \Diamond B)) $$ Roughly, this says that the ...
5
votes
1answer
85 views

A function is lambda-2-definable iff it is HG computable and provably type correct in lambda-PRED2

I'm having a problem regarding Theorem 5.4.40.3 of Barendregt's Lambda calculi with types (1992), a chapter in Handbook in logic in computer science. (I'm referring to the PostScript version available ...
6
votes
0answers
82 views

What is known about reduction by “$P_1$ interprets $P_2$” for generalized programming languages?

Inspired by this answer, let's say that a programming language is given by the data $L=(P,ev)$ where $P$ (the set of "valid programs") is a computable subset of $\Sigma^*$ and $ev$ (the "evaluator") ...
4
votes
2answers
108 views

Is there a mathematical analysis/proof available for correctness of solutions to inter process communication problems?

I've been going over some material related to IPC recently from Tanenbaum's "Modern Operating Systems" and revisited semaphore after many years. There is a lot of code and pseudo code based ...
5
votes
4answers
129 views

Use of Process Calculi and PL Theory for modern programming language development

For a while now, I have been very interested in programming language theory and process calculi and have started to study them. To be honest, it something that I wouldn't mind going into for a career. ...
7
votes
1answer
120 views

Are there stronger notions of equivalence over lambda terms than beta equivalence?

I should add the context that I am concerned with strongly normalizing systems like System-F. I have what I consider a very strong notion of equivalence for lambda terms that goes something like the ...
3
votes
1answer
83 views

Is it possible to determine if a reduction is correct?

Suppose we have an arbitrary term, x, in Lambda Calculus, or in an equivalent turing-complete system. Suppose we ask an oracle what is the normal form of that term, ...
1
vote
0answers
61 views

Object-Oriented Programming Languages based on assignment

Is it correct to claim that an object-oriented programming language based on assignment (e.g., Java and Smalltalk) introduces mutability and hence complexity in concurrent applications ? In other ...
2
votes
2answers
129 views

Would it be possible for a compiler to convert a recursive sum into the average formula?

def sum1(n): if n==0: return 0 else: return n + sum1(n-1) def sum2(n): return n*(n+1)/2 A compiler can not convert ...
2
votes
0answers
107 views

How useful is program search in the field of programming-language theory?

I've been thinking: computing systems such as the Lambda Calculus and its variations are usually very simple and can be implemented in as few as ~80 lines of Haskell code. There is a self-interpreter ...
1
vote
0answers
63 views

Is there any system where function equality (extensionality) is decidable?

Is there any programming language or system where function equality (extensionality) is decidable?
10
votes
0answers
202 views

A bijection between ordered lambda terms and rooted planar maps?

Consider the following recurrence in two parameters $n$ and $k$: \begin{aligned} NF(0,k) &= 0 \\ NF(n,k) &= Neu(n,k) + NF(n-1,k+1) \\ Neu(n,k) &= [n=1 \wedge k=1] + ...
4
votes
4answers
248 views

How to introduce recursion to Simply Typed Lambda Calculus while at the same time keeping strong normalisation?

Suppose you have a version of the STLC with one base type, similar to: data Tree = Branch Tree Tree | Leaf Now, suppose you want to add recursion to that ...
4
votes
0answers
110 views

Is there a programming language where any arbitrary recursive function can be fused?

Compilers like GHC for Haskell use inlining as one of its most important optimising tools. Doing that is not possible for recursive functions, in general. A few techniques have been developed to amend ...
5
votes
0answers
126 views

Complete combinator basis for System F-omega

The S and K combinators form a complete (and Turing complete) basis when untyped. Within the Hindley-Milner type-system, and I believe within system $F$ as well, S and K can encode any well-typed ...
2
votes
1answer
67 views

Language with extensible type system?

Is there a practical programming language that has an extensible type system? Or alternatively, an add-on type system that can be used with existing languages? With extensible I mean that the typing ...
7
votes
1answer
113 views

Decidability of inductive invariant existence in Presburger arithmetic

Problem: Consider a finite number of control states (including an "initial" and a "bad" state), a finite number of integer variables, and for each ordered pair of states a transition relation ...
4
votes
1answer
317 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 ...
3
votes
2answers
100 views

Well-formedness condition for inductive types

I work on implementing a simple dependently typed language. I want to implement inductive types there. However, I want them to be well formed. From what I've seen in Coq not all types are acceptable. ...
7
votes
1answer
187 views

Algorithm to determine function equality on the simply typed lambda calculus?

We know that beta-equality of simply typed lambda-terms is decidable. Given M,N:σ→τ, is it decidable whether for all X:σ, MX $≃_β$ NX?
11
votes
1answer
182 views

Can we distinguish strictly syntactic and semantic methods in programming language?

While discussion strong normalization proofs, this comment contrasts the "normal forms model" with "purely syntactic methods". This brings me back to a more basic question: can we still distinguish ...
9
votes
1answer
152 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 ...
4
votes
1answer
124 views

Is it possible to create an algorithm-aware optimizer?

I've recently implemented a physics system where each object has to interact with eachother. It consisted of, pretty much, the following algorithm: ...
1
vote
1answer
145 views

What's the relation between OOP and category theory?

What's the relation between OOP and category theory? Is there some related work on this topic one can read?
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 ...
2
votes
0answers
29 views

Are the sets of executions of data-race free programs equal, when run on causal memory and on sequentially consistent memory respectively?

In the paper "Causal Memory: Definitions, Implementations, and Programming (Distributed Computing [DC] 1995)", the authors present a formal definition of causal memory, an abstraction of distributed ...
1
vote
1answer
118 views

How can an inherited attribute be simulated using a synthesized attribute?

Is it possible to simulate an inherited attribute using a synthesized attribute? For example, can the inherited attribute SYMTAB used in normal code generation modules be simulated using a synthesized ...
6
votes
1answer
164 views

Homoiconic languages which are not Turing complete

Does there exist a programming language which is homoiconic (in the sense that any code can be represented as a data structure, can be altered, and can be run after being altered) but not Turing ...
4
votes
2answers
142 views

Higher order Quines - when do super Quines exist?

The normal Quine - a program that prints its own code - is a special case of an n-Quine. An n-Quine is a program that prints code for a different program that after n iterations of printing and ...
2
votes
1answer
60 views

Conditional Dependencies in Compiler Semantic Analysis Passes

Imagine that we have a been given an Excel spreadsheet with three columns, labeled COND, X and Y. ...
2
votes
2answers
163 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 ...
4
votes
3answers
279 views

How to make the Lambda Calculus strong normalizing without a type system?

Is there any system similar to the lambda calculus that is strong normalizing, without the need to add a type system on top of it?
7
votes
3answers
347 views

Can one automate algorithmic analysis?

Has anyone thought about the possibility of a programming language, and a compiler, such that the compiler can automatically do worst-case asymptotic analysis? The use case I have in mind is a ...
3
votes
1answer
328 views

In what sense are Scala's Try[T] and Future[T] dual?

In a recent course based on Scala I found a hint that the Scala types Try[T] and Future[T] are dual. This was explained only ...
3
votes
3answers
198 views

Is there a language with strong typed interfaces where types resolution are “delayed”?

I know that this question it not entirely theoretical, but I think that's the place where is more probable that someone knows the answer. The question is: is there any OO strong typed language where ...
8
votes
2answers
349 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 ...
2
votes
0answers
71 views

Evaluation contexts: outside-in vs inside-out

I heard that there exist two styles to define an evaluation context: outside-in and inside-out. Can someone give the definitions? Why are they so named (inside-out and outside-in)? What is the ...
6
votes
2answers
283 views

What is the goal behind abstract interpretation in programming languages?

I am now trying to understand better what "abstract interpretation" in programming languages are. I found a good book chapter that explains the idea of extending the domain with a least fixed element, ...
1
vote
3answers
312 views

Is there an array structure that allows for O(1) complexity for reverse, zip, slice etc operations?

Many operations on arrays have $O(n)$ complexity. If we represent arrays as accessors methods, many of them could be done in $O(1)$. For example, the $i$th item in the reverse of an array $A$ of ...
0
votes
0answers
38 views

What are some properties of the function that computes the ratio of the first N Jot programs that halt?

Let S(N) be a set of the first N programs in Jot. Suppose that F is function that returns an approximation of the ratio of programs in a set that halt (we can guess ...
2
votes
2answers
197 views

Is there a space efficient way to represent numbers on the lambda calculus?

This is something I've been thinking. While it is agreed that Lambda Calculus is equivalent to a Turing Machine in power, is it actually so? Church Numerals are not very space efficient and I'm not ...
3
votes
2answers
141 views

Reversing the CPS transformation?

A quick Google search didn't turn up anything obvious, so I'm asking here. Converting direct style programs to continuation-passing style is a well-studied program transformation. However, I'm ...
1
vote
3answers
171 views

Is there any language for which a perfect optimization is decidable?

Is there a programming language L where it is possible to write an optimizer O, that, receiving a program in L and a set of cost for every low-level operation in L, returns the equivalent program with ...