Questions tagged [pl.programming-languages]

Programming languages, in particular, focussing on their semantics.

Filter by
Sorted by
Tagged with
32
votes
4answers
15k 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
197 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
932 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 ...
1
vote
4answers
927 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
757 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
118 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 ...
3
votes
2answers
350 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
752 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 ...
1
vote
1answer
472 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: http://www.eecs.ucf....
7
votes
1answer
221 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 ...
10
votes
1answer
314 views

Literature on alias analysis

I am writing my master's thesis in CS and I am working with alias analysis. The thing that I am interested in is intraprocedural, flow sensitive must- and may-alias analysis for Java-like languages. ...
6
votes
3answers
252 views

Preserving termination when rewriting recursive programs

Powerful program transformations like partial evaluation, deforestation and supercompilation are based on applying three kinds of transformations: Rewrite using axioms, e.g. a+b = b+a. Unfolding/...
4
votes
1answer
1k views

Defining Mutually Recursive functions in Coq

This question is related to (but not the same as): How to define a function inductively on two arguments in Coq? In particular, I used those techniques (defining a second fixed point function) and ...
9
votes
2answers
862 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 ...
24
votes
6answers
2k views

How should I think about proof nets?

In his answer to this question, Stephane Gimenez pointed me to a polynomial-time normalization algorithm for proofs in linear logic. The proof in Girard's paper uses proof nets, which are an aspect of ...
5
votes
0answers
256 views

Commonalities and differences between canonical structures and the implicit calculus

There is a paper on The Implicit Calculus as a generalization of type classes. Coq's canonical structures are also a generalization of type classes. The paper does not mention canonical structures ...
15
votes
1answer
451 views

Is MALL + unrestricted recursive types Turing-complete?

If you look at the recursive combinators in the untyped lambda-calculus, such as the Y combinator or the omega combinator: $$ \begin{array}{lcl} \omega & = & (\lambda x.\,x\;x)\;(\lambda x.\,x\...
5
votes
4answers
3k views

Is there such a thing as a state-based programming language?

As anyone knows who has read Alan Turing's paper describing the Turing Machine (On Computable Numbers, With an Application to the Entscheidungsproblem), the syntax he uses is vastly different from ...
2
votes
3answers
227 views

References on model checking and pi calculi

I'm a mathematician and it looks like I need to learn about these topics. What would be good references that go into the technical details of the following topics? (s)pi calculus model checking I'm ...
4
votes
0answers
133 views

What are the parts of consistency model playing in hardware, operating system, and programming language?

In multiprocessor programming, consistency model is the key concept to express the correctness of concurrent objects ranging from simple read/write shared variable to concurrent data structures like ...
8
votes
2answers
274 views

Simply-stated restriction on imperative programming language that captures the elementary functions?

The language of while programs can express the computably enumerable functions. (This is true even if the only arithmetical operations on variables are, say, ...
2
votes
3answers
2k 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 ...
5
votes
2answers
286 views

Why do we need PAP (partial aplication) objects in heap?

In the paper “Making a Fast Curry: Push/Enter vs. Eval/Apply for Higher-order Languages” by Simon Marlow and Simon Peyton Jones it is told that a PAP heap object may be created in the push/enter model ...
8
votes
2answers
251 views

Resumption-based IO systems?

I've been playing around with resumptions lately, mostly from Abramsky's classic paper Retracing Some Paths in Process Algebra. They are quite slick (basically solutions to the domain equation $R = I \...
5
votes
1answer
138 views

Partial soundness proofs for pragmatic static analyses

I was reflecting on a comment by Rob Simmons on unsound static analyses: An analysis that is neither sound nor complete is called pragmatic by Jaspan, as there aren't any theorems to be proved ...
9
votes
1answer
808 views

Will Martin-Löf Type Theory lead to a greater ability to write provably correct code?

This post refers to the Curry-Howard isomorphism and the Martin-Löf Type Theory. The post makes the claim of a future 'unification' between the the describing language of math, and the operation ...
6
votes
1answer
250 views

In what sense are coroutines dual to (sub)routines?

The name coroutine suggests that in some sense they should be dual to (sub)routines. Is there a real mathematical duality? I'm hoping for something like "in category theory subroutines are X and ...
0
votes
1answer
131 views

How to generalize a map of type for many operators?

I am formalizing the type system for a small language, and thus writing inference rules. Taking unary - operator for example, its entry may be a number as well as ...
22
votes
1answer
1k views

How are Futures described in terms of category theory?

Is there a useful description of futures or promises in terms of category theory? In particular, what could the categorical dual of Future be?
2
votes
1answer
122 views

How to auto-derivate sequential iterative programs from a mathematical specification?

I had to derivate, by hand, sequential iterative programs at school using an unified Hoare-Dijkstra-Hehner programming theory. First, write down the formal specification as a Hoare triple and figure ...
6
votes
1answer
414 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 ...
10
votes
1answer
2k 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 ...
13
votes
1answer
444 views

Is contextual equivalence of a language with `quote`-`eval` trivial or not?

In [1], Mitchell Wand demonstrated that adding fexprs to the pure lambda calculus trivializes the theory of contextual equivalence, meaning two terms are contextually equivalent iff they are $\alpha$-...
12
votes
2answers
634 views

What are the relations between Alternative, MonadPlus(LeftCatch) and MonadPlus(LeftDistributive)?

Following up What’s an example of a Monad which is an Alternative but not a MonadPlus?: Assume $m$ is a monad. What are the relations betweem $m$ being an Alternative, a MonadPlusCatch and a ...
19
votes
2answers
2k views

What are the limits of total functional programming?

What are the limitations of total functional programming? It is not Turing-complete, but still supports a large subset of the possible programs. Are there important constructs that you could write in ...
9
votes
3answers
731 views

Is it possible to compute whether two functions are extensional equal?

If you have two functions implementing a different sorting algorithm, is it then possible to infer by source code that they both have the same external properties? Meaning that they both will have a ...
13
votes
3answers
717 views

Can any program be implemented mechanically?

Is it possible to build a single purpose (non Turing complete) mechanical implementation of say, Microsoft Word? Is it possible to implement such things as iterators, first-order functions, the whole ...
1
vote
2answers
207 views

Is there a computation class describing FOR-programs, what are the limitations?

I've written an unpublished paper that describes FOR-programs. FOR-programs are programs that only contain bounded for loops and basic operations (assignment, addition, multiplication, etc.). A ...
18
votes
3answers
490 views

Frame rule as a change-preserver?

A frame rule, like the one given below, captures the idea that, given a program c with precondition p that holds before it runs ...
8
votes
2answers
351 views

Original Hoare Logic termination paper

I'm looking for the original paper where Hoare (or someone else I suppose) discusses termination (Total Correctness). Or any other early work on termination for "vanilla" Hoare logic (I suppose by ...
7
votes
1answer
444 views

Papers on Prolog-like languages without closed world assumption (CWA)

Prolog execution process may be seen as a search that model scientific search for a proof of a proposition. At the same time, real world scientific search greatly differs from Prolog search in the ...
9
votes
1answer
443 views

What are possible implementations of Haskell's type classes and what are their (dis)advantages?

As far as I know, a Haskell function with type classes constraints is internally compiled to a function with additional arguments that receive dictionaries with the necessary implementations of each ...
4
votes
1answer
283 views

Classes and types in object-oriented languages

In typical object-oriented programming languages like Java, classes are used as types. On the other hand, type-theoretic approaches to object-oriented languages treat interfaces as types. Are there ...
10
votes
2answers
827 views

Ownership types and Separation Logic

Ownership types and Separation Logic seem to have similar goals, control over ownership and aliasing. Perhaps, I should also add: the ability to write modular specifications. What is known about the ...
11
votes
3answers
5k views

Programming Language Theory and Abstract Algebra

Are there any applications of Abstract Algebra to Programming Language Theory? Is there anything that would be useful in language design and compiler implementation?
4
votes
1answer
363 views

Formal Representation of Haskell Data-Types

I come from Haskell programming and currently writing my (Diploma/Master) thesis. I'm having trouble finding a formal/mathematical notation for a Haskell data-type. The Haskell data type is: ...
8
votes
1answer
334 views

Proofs techniques related to Curry–Howard correspondence

I am looking for sources about formalized notion of programs. This seems to be closely related to Curry-Howard correspondence, but one could also track this back to Universal Turing Machines and its ...

1 2 3
4
5
7