Programming languages, in particular, focussing on their semantics.
12
votes
2answers
210 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
70 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 ...
2
votes
3answers
370 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 ...
0
votes
0answers
14 views
What is a sort in Programming Language Semantics? [migrated]
I've started reading Practical Foundations for Programming Languages and in the first chapter, the author mentions that ast's are associated with sorts. Intuitively, sorts are like types, but I'd like ...
8
votes
2answers
355 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
79 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
204 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
120 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 ...
17
votes
2answers
2k 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
112 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
97 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
82 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
208 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
125 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.
...
4
votes
2answers
409 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
569 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
146 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
231 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
183 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
72 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
161 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
262 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
118 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
150 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
69 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
254 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
132 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
91 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
389 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
87 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
283 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
294 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
205 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
105 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
310 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
182 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
538 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
168 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
335 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
224 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
209 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
202 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
185 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
279 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 ...
8
votes
3answers
2k 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?
3
votes
1answer
279 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:
...
7
votes
1answer
224 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 ...
5
votes
1answer
157 views
Characterizing closure under expansion/reduction for big-step semantics?
Two common ways of formulating operational semantics for programming languages based on lambda-calculus are big-step and small-step semantics.
In a big step semantics, you give a relation $e ...
7
votes
4answers
166 views
Early References for Transition System Semantics of Programs
I am trying to trace back the origins of transition system semantics for imperative programs. I am assuming a transition system is a tuple $(\mathit{States}, \mathit{Trans})$ consisting of a set of ...
