Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [pl.programming-languages]

Programming languages, in particular, focussing on their semantics.

3
votes
0answers
163 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 ...
3
votes
0answers
230 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
283 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] + \sum_{l=1}^{n-1}\sum_{...
5
votes
4answers
1k 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 ...
7
votes
0answers
214 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 ...
8
votes
0answers
383 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 ...
3
votes
1answer
387 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 ...
8
votes
1answer
179 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 ...
5
votes
1answer
1k 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 ...
4
votes
2answers
145 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. ...
10
votes
1answer
620 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?
14
votes
1answer
463 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 ...
10
votes
1answer
178 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
153 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: ...
5
votes
3answers
2k 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
224 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
97 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
511 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 ...
7
votes
1answer
497 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 ...
5
votes
2answers
182 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
91 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. ...
3
votes
2answers
238 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 ...
9
votes
3answers
1k 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?
8
votes
3answers
429 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 ...
5
votes
1answer
1k 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
236 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 ...
15
votes
2answers
1k 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
127 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 ...
9
votes
2answers
1k 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
617 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 ...
3
votes
2answers
642 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
244 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 ...
2
votes
3answers
250 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 ...
2
votes
3answers
323 views

Is there any programming language in which any equivalent program has a unique, decidable normal representation?

Is there any programming language in which any equivalent program has a unique normal representation, and that normal representation is decidable? Is other words, suppose A and B are programs ...
1
vote
1answer
235 views

A few questions about ISWIM

I recently read Landin's paper "The Next 700 Programming Languages". But I was a bit confused by ISWIM. In particular, are functions first-class objects in ISWIM? It seems not because every ...
4
votes
1answer
347 views

Aren't Monads F-Algebra's? And then if that could be said are Comonad's F-Coalgebra's?

So considering a Monad to be a Triple (T:C -> C, η, µ) with eta and mu as the Natural transformations with appropriate signatures, isn't this in essence an F-Algebra? My thinking is that being both (...
5
votes
3answers
1k views

How to measure programming language succinctness?

I want to explore the notion of quantifying the amount of succinctness a programming language provides. That is, the amount a high-level language reduces the complex. This idea of "simplification" ...
5
votes
2answers
658 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 am ...
0
votes
1answer
168 views

Static structure of program

Firstly, I admit that my question is just something very blurred but I hope someone please give me some documents to read. The execution of a program $P$ can be considered as a sequence of state ...
32
votes
4answers
14k views

Research and open challenges in Programming Language Theory

In the spirit of some general discussions like this one, I'm opening this thread with the intention to gather opinions on what are the open challenges and hot topics in research on programming ...
3
votes
1answer
186 views

State-of-the-art unification for associative-commutative functions

I am interested what are the open problems on unification methods for associative-commutative functions, and what is the state-of-the-art work? I have found some old work, but nothing new. I am ...
23
votes
4answers
2k views

When does (or should) Theoretical CS care about intuitionistic proofs?

From what I understand (which is very little, so please correct me where I err!), theory of programming languages is often concerned with "intuitionistic" proofs. In my own interpretation, the ...
14
votes
1answer
844 views

η-conversion vs extensionality in extensions of lambda-calculus

I'm often confused by the relation between η-conversion and extensionality. Edit: According to comments, it seems I'm also confused about the relation between extensional equivalence and ...
0
votes
4answers
894 views

A simple programming language?

What is a simple toy research programming language that has simple denotational semantics (including numbers or reals) that is used often to demonstrate certain properties of programming languages, or ...
9
votes
2answers
753 views

Formal representation of an abstraction hierarchy

Introduction I'm writing my PhD thesis on Abstract Delta Modeling (ADM), an abstract algebraic description of modifications (known as deltas) able to act on products (as in 'software products'). This ...
5
votes
0answers
117 views

conceptual tools for illustrating types of computation?

From time to time I come across concepts in programming that take a certain number of exposures to grasp. Things like: tail calls, futures, monads, coroutines, closures, call/cc. The common theme is ...
2
votes
2answers
306 views

Undecidability of program optimization

A program is an encoded Turing Machine. And a size optimizer of a program is a TM $M_1$ such that: On any input $M$, $M_1$ outputs $M_{min}$ such that $M_{min}$ is the shortest TM which is ...
2
votes
1answer
239 views

A few questions about Object-Oriented Languages in general

I was not a big fan of Object-Oriented Languages (OOL), but recently started to learn a bit more about their pros and cons in a general setting instead of diving into one such language. I have a few ...
27
votes
2answers
4k views

What is the logarithm or root operation in type-space?

I was recently reading The Two Dualities of Computation: Negative and Fractional Types. The paper expands on sum-types and product-types, giving semantics to the types ...
7
votes
1answer
731 views

Constraint types (IBM/X10) compared to dependent types

Constraint types have been proposed by IBM in their X10 programming language (it's a commercial programming language, not open source software). Nystrom, Nathaniel, et al. "Constrained types for ...