Skip to main content

Questions tagged [pl.programming-languages]

Programming languages, in particular, focussing on their semantics.

Filter by
Sorted by
Tagged with
3 votes
2 answers
280 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 ...
zhuang's user avatar
  • 31
6 votes
0 answers
280 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 ...
Bob's user avatar
  • 381
5 votes
1 answer
574 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 <...
Benjamin Kovach's user avatar
8 votes
1 answer
144 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 ...
Neel Krishnaswami's user avatar
6 votes
1 answer
133 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 ...
Pteromys's user avatar
  • 895
9 votes
1 answer
172 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") ...
Joshua Grochow's user avatar
5 votes
2 answers
199 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 ...
vin's user avatar
  • 161
11 votes
5 answers
1k 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. ...
Stefan G.'s user avatar
  • 241
7 votes
1 answer
363 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 ...
Jake's user avatar
  • 1,203
3 votes
1 answer
109 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, ...
MaiaVictor's user avatar
  • 3,147
1 vote
0 answers
111 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 ...
Sergio's user avatar
  • 111
2 votes
2 answers
235 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 ...
MaiaVictor's user avatar
  • 3,147
3 votes
0 answers
176 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 ...
MaiaVictor's user avatar
  • 3,147
3 votes
0 answers
403 views

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

Is there any programming language or system where function equality (extensionality) is decidable?
MaiaVictor's user avatar
  • 3,147
11 votes
0 answers
306 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_{...
Noam Zeilberger's user avatar
6 votes
4 answers
2k 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 ...
MaiaVictor's user avatar
  • 3,147
7 votes
0 answers
225 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 ...
MaiaVictor's user avatar
  • 3,147
9 votes
0 answers
525 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 ...
Jake's user avatar
  • 1,203
3 votes
1 answer
587 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 ...
user22525's user avatar
8 votes
1 answer
202 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 ...
David Monniaux's user avatar
6 votes
1 answer
2k 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 languages are object oriented languages, but one of them a multiparadigm language because it supports ...
bitli's user avatar
  • 163
4 votes
2 answers
200 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. ...
Konstantin Solomatov's user avatar
10 votes
1 answer
1k 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?
MaiaVictor's user avatar
  • 3,147
16 votes
1 answer
638 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 ...
Blaisorblade's user avatar
  • 2,059
10 votes
1 answer
226 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 ...
Opt's user avatar
  • 1,311
4 votes
1 answer
159 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: ...
MaiaVictor's user avatar
  • 3,147
8 votes
3 answers
4k 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?
qazwsx's user avatar
  • 559
2 votes
2 answers
304 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 ...
TomR's user avatar
  • 409
2 votes
0 answers
106 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 ...
hengxin's user avatar
  • 2,329
2 votes
1 answer
1k 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 ...
saikat's user avatar
  • 175
7 votes
1 answer
547 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 ...
Bruno Le Floch's user avatar
5 votes
2 answers
207 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 ...
Lucas's user avatar
  • 159
2 votes
1 answer
101 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. ...
n00b101's user avatar
  • 369
3 votes
2 answers
310 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 ...
user's user avatar
  • 615
12 votes
3 answers
2k 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?
MaiaVictor's user avatar
  • 3,147
9 votes
3 answers
491 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 ...
manoj's user avatar
  • 341
5 votes
1 answer
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 ...
Giorgio's user avatar
  • 151
3 votes
3 answers
297 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 ...
castarco's user avatar
  • 143
18 votes
2 answers
2k 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 ...
Phillip Mates's user avatar
2 votes
0 answers
203 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 ...
day's user avatar
  • 2,805
10 votes
2 answers
2k 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, ...
newToPL's user avatar
  • 103
1 vote
3 answers
633 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 ...
MaiaVictor's user avatar
  • 3,147
3 votes
2 answers
938 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 ...
MaiaVictor's user avatar
  • 3,147
4 votes
2 answers
366 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 ...
Neel Krishnaswami's user avatar
2 votes
3 answers
298 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 ...
MaiaVictor's user avatar
  • 3,147
2 votes
3 answers
351 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 ...
MaiaVictor's user avatar
  • 3,147
2 votes
2 answers
331 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 ...
day's user avatar
  • 2,805
4 votes
1 answer
431 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 (...
Mzk Levi's user avatar
  • 143
5 votes
3 answers
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" ...
TheDoctor's user avatar
  • 159
5 votes
2 answers
746 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 ...
Lii's user avatar
  • 211

1 2 3
4
5
8