Programming languages, in particular, focussing on their semantics.
3
votes
0answers
110 views
What kinds of programming pitfalls modern languages are able to express?
I often see claims that modern functional strictly-typed languages are 'safer' than others. These statement mostly linked with type systems and their ability to explicitly express the following ...
3
votes
2answers
175 views
How to measure programming language expressiveness?
I want to explore the notion of quantifying the amount of expressiveness a programming language provides. That is, the amount a high-level language reduces the complex.
This idea of ...
5
votes
2answers
224 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
103 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 ...
8
votes
4answers
571 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
72 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 ...
14
votes
4answers
661 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 ...
7
votes
0answers
83 views
η-conversion vs extensionality in extensions of lambda-calculus
I'm often confused by the relation between η-conversion and extensionality.
In the untyped lambda-calculus, the eta-rule gives the same proof system as the extensionality rule, as proven by ...
0
votes
4answers
485 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 ...
8
votes
2answers
370 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
83 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
207 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
129 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 ...
18
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
159 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
101 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:
...
5
votes
1answer
89 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 ...
6
votes
1answer
214 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.
...
5
votes
3answers
129 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.
...
5
votes
2answers
416 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 ...
15
votes
5answers
589 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 ...
4
votes
0answers
151 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 ...
13
votes
1answer
239 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 ...
3
votes
4answers
2k 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
186 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 ...
2
votes
0answers
75 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(or safety) of concurrent objects ranging from simple shared variable to concurrent data structures like ...
7
votes
2answers
163 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, ...
1
vote
3answers
280 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
120 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 ...
7
votes
2answers
154 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 ...
4
votes
1answer
70 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 ...
6
votes
1answer
260 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 ...
5
votes
1answer
138 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 ...
1
vote
1answer
96 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 ...
17
votes
1answer
402 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
90 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 ...
4
votes
1answer
286 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 ...
6
votes
1answer
322 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 ...
11
votes
0answers
207 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 ...
5
votes
2answers
109 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 ...
7
votes
2answers
330 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 ...
3
votes
3answers
193 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 ...
12
votes
3answers
547 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
172 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 ...
17
votes
3answers
343 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 ...
9
votes
2answers
225 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 ...
4
votes
1answer
213 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
209 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
186 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 ...
9
votes
2answers
283 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 ...
