Programming languages, in particular, focussing on their semantics.

learn more… | top users | synonyms (2)

1
vote
0answers
26 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
0answers
29 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
97 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
255 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
84 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. ...
1
vote
0answers
52 views

Lambda calculus: difference between contexts and evaluation contexts [migrated]

Firstly, I'd like to say that my text below may contain errors, so feel free to point out any mistakes in my formulation of the question. Consider an untyped lambda calculus with booleans and ...
7
votes
1answer
154 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?
-3
votes
0answers
23 views

Fortran90 specific question [migrated]

I have a question specifically about Fortran 90. I am busy extracting large ammounts of data and trying to read it out. How do I read only one column out of 30?
8
votes
1answer
140 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
144 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
119 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
94 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
61 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
18 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
98 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 ...
5
votes
1answer
97 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 ...
3
votes
0answers
73 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
47 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
146 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
222 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
337 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
222 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
191 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
293 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 ...
1
vote
0answers
67 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
237 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
284 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
171 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
126 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
161 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
249 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
114 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 ...
3
votes
1answer
163 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 ...
3
votes
2answers
398 views

How to measure programming language succintness?

I want to explore the notion of quantifying the amount of succintness a programming language provides. That is, the amount a high-level language reduces the complex. This idea of "simplification" ...
5
votes
2answers
354 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 ...
0
votes
1answer
137 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 ...
12
votes
4answers
2k 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
110 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 ...
15
votes
4answers
861 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 ...
8
votes
1answer
226 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
580 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
542 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
107 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
233 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
184 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 ...
20
votes
2answers
3k 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 ...
6
votes
1answer
360 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 ...
0
votes
1answer
166 views

Verification: how 'formal' is a tool like Java Modeling Language (JML) compared to certified libraries and model checking?

(note: this is probably a beginner question, and English is not my first language) Recently, I have read a paper that used the “Java Modeling Language” (JML), see for instance: ...
6
votes
1answer
111 views

Step-indexing: Where to begin?

I am about to begin a verification project (for MIPS) with my professor (I am a senior undergraduate) and have been told that the soundness proof for the program logic we need will probably involve ...