Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [pl.programming-languages]

Programming languages, in particular, focussing on their semantics.

1
vote
1answer
437 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....
6
votes
1answer
184 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
309 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
249 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
847 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
255 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
416 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
129 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
262 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
278 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
244 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
136 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
785 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
237 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
967 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
405 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
424 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$-...
11
votes
2answers
589 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
654 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
697 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
204 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
462 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
338 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 ...
6
votes
1answer
424 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
439 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
276 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
777 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 ...
10
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
359 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
320 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
244 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
245 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 ...
16
votes
1answer
357 views

Parametricity and projective eliminations for dependent records

It's well-known that in System F, you can encode binary products with the type $$ A \times B \triangleq \forall\alpha.\; (A \to B \to \alpha) \to \alpha $$ You can then define projection functions $\...
15
votes
2answers
320 views

Uses of quasi-PERs/difunctional relations/zig-zag relations?

Given sets $A$ and $B$, a difunctional relation $(\sim) \subseteq A \times B$ between them is defined to be a relation satisfying the following property: If $a \sim b$ and $a' \sim b'$ and $a \sim ...
3
votes
1answer
75 views

Research papers regarding disinterval analysis

I'm trying to implement a disinterval analysis similiar to what is described in Clousot: Static Contract Checking with Abstract Interpretation (under section 5.2) - and I'm trying to find some papers ...
15
votes
4answers
543 views

Unary parametricity vs. binary parametricity

I've recently become quite interested in parametricity after seeing Bernardy and Moulin's 2012 LICS paper ( https://dl.acm.org/citation.cfm?id=2359499). In this paper, they internalize unary ...
3
votes
1answer
378 views

What can the Haskell package category-extras be used for?

See here. Has anyone attempted to use this to verify category theoretic proofs? Given the relationship between categories and graphs, are there some applications with respect to graph algorithms? What ...
5
votes
1answer
475 views

What are the limitations on formal proofs of Erlang systems?

Well, today I just got my 15 minutes of fame, but now I think I am wrong on the point about formal proofs on Erlang systems. The discussion on news.ycombinator.com suggests that Erlang code may or ...
9
votes
2answers
1k views

Formal Definition/counter part in mathematics for “Objects” of Object Oriented Models

This is a question I asked in mathematics SE forum, and I was referred here. So here is the question- I'm a newbie in both formal mathematics and theoretical computer science, so please bear with me ...
10
votes
1answer
235 views

Unification-based elimination rule for equality

A few years back, I ran across the following left-rule for equality in sequent calculus: $$ \frac{s \doteq t \leadsto \theta \qquad \theta(\Gamma) \vdash \theta(C)} {\Gamma, s \doteq t ...
4
votes
3answers
843 views

What advantages does having a null-able string type confer to a programming language?

I've been trying to understand the rationale behind the design of the C# language. Are there any specific advantages that can be gleaned from allowing string type variables to contain null?