# Questions tagged [pl.programming-languages]

Programming languages, in particular, focussing on their semantics.

54 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
265 views

### Generalizing limit-colimit coincidence to Scott-continuous adjunctions: any uses?

In Abramsky and Jung's 1994 handbook chapter on denotational semantics, after proving that the limit and colimit of expanding sequences exist and coincide, they have the following to say about ...
• 32.6k
306 views

### A bijection between ordered lambda terms and rooted planar maps?

Consider the following recurrence in two parameters $n$ and $k$: \begin{aligned} NF(0,k) &= 0 \\ NF(n,k) &= Neu(n,k) + NF(n-1,k+1) \\ Neu(n,k) &= [n=1 \wedge k=1] + \sum_{l=1}^{n-1}\sum_{...
• 4,561
227 views

### What is the "standard" lambda-calculus model for bicartesian closed categories?

(I'm familiar with the lambda-calculus, less so with its categorical models.) It is well-known that cartesian-closed categories are in tight correspondence to the simply-typed lambda-calculus with ...
• 2,040
438 views

### Typed Lambda Calculus models and denotations

I'm trying to draw a general mental picture about the models and the denotational semantics of the typed lambda calculus, in its different variants. I'm particularly interested in how the semantics ...
• 678
128 views

### Does Bellantoni-Cook safe recursion (or any other implicit characterization of P) admit Kleene's second recursion theorem?

Abstractly, by a programming language that operates on binary strings I mean a set $P$ of programs along with a semantics relation $[p](x) = y$, the program $p$ on string $x$ halts with output $y$.&...
• 851
526 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 ...
• 1,203
443 views

### Type inference with subtype constraints and polymorphism using Trifonov and Smith's constraint maps

Trifonov and Smith's Subtyping Constrained Types (1996) introduces constraint maps to represent consistent closed constraint sets (such maps providing sets of lower and upper bounds to each variable ...
• 1,379
139 views

### Halting problem for finitary PCF

Is the halting problem decidable for finitary PCF? By "halting problem" I mean the problem of deciding whether a closed PCF term evaluates to bottom under the denotational semantics of PCF. ...
• 71
231 views

### Relationship between Pataraia's theorem and inductive-recursive definitions?

Pataraia's fixed point theorem gives a constructive proof of the fact that if you have a monotone function $f$ on a DCPO, then it has a least fixed point. I've frequently used this fixed point theorem ...
• 32.6k
225 views

### Is there a programming language where any arbitrary recursive function can be fused?

Compilers like GHC for Haskell use inlining as one of its most important optimising tools. Doing that is not possible for recursive functions, in general. A few techniques have been developed to amend ...
• 3,157
115 views

### List Functions That Don't Depend on Length

Intuitively, a polymorphic function of type $f : \forall a. [a] \to [a]$ cannot inspect the type of its elements. This intuition can be captured formally using either natural transformations or ...
• 93
183 views

### Notions of Computability at Higher Type III

I've recently found a very nice survey paper called "Notions of Computability at Higher Type" by John R. Longley. The paper says it is part of a 3-part series, with the 3rd concerning non-extensional ...
• 1,695
462 views

### How can unification be applied to interaction combinators?

The problem of unifying interaction combinators is probably undecidable since those are turing complete. As opposed to the lambda calculus, there is nothing like a simple type theory for interaction ...
• 3,157
282 views

N.B. I asked the same question on Stack Overflow but it was suggested that it is too theoretical for this forum. It is great that Haskell allows us to walk around in the category $Hask$. But ...
• 381
168 views

### Can a positive elementary inductive definition refer to its own stage comparison relation?

Moschovakis' stage comparison theorem says that the stage comparison relation associated with any positive elementary induction is itself definable by (another) positive elementary induction. But what ...
• 851
122 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 ...
• 151
258 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 ...
• 390
83 views

### Description of the CPS transformation for the typed lambda-calculus

Is there somewhere a precise but hopefully readable account of how the CPS (=continuation-passing-style) transformation applies to the typed lambda-calculus? (Say, simply-typed with product and sum ...
• 841
56 views

### Coinduction principle for smash products of pointed cpos

In "Relational Properties of Domains", Pitts gives a coinduction principle for pointed cpos (cppos). In corollary 6.13 (below), he specializes it to cppos constructed as fixed points of cppo-...
120 views

### Proof that CIC or Dybjer-style eliminators are strongly-normalizing?

Related to this question I'm wondering, what is the standard technique for showing that dependent types with eliminators are strongly normalizing? I'm thinking something like the Calculus of ...
• 2,942
169 views

### Hereditary Substitution with Inductives and Eliminators?

I'm wondering, is there any existing work on hereditary substitution with inductive type families and dependent eliminators? In particular, normalizing the application of an eliminator to an ...
• 2,942
136 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 ...
• 2,329
51 views

### Are there any programming languages based on the method of analytic tableaux, aside from Fitting's Proflog?

The method of analytic tableaux [0] describes a process by which logical formulae, particularly of first order logic, can be determined to be valid or invalid. From the Wikipedia entry: A tableau ...
• 111
171 views

### syntax and semantics for transfinite algorithms

Let's say I wanted to informally describe a very simple algorithm for searching through an (undirected) finite connected graph $G = (V,E)$. I could define, for each natural number $n$, a set $S_n$ and ...
• 851
156 views

### Set:Set or Negative Inductives in a Total Language?

In total dependently typed languages, general recursion is forbidden, since this can allow for non-terimination. However, dependently typed language can still describe Turing-complete computations (...
• 2,942
128 views

1 vote
81 views

### Decision vs search problem specification

Let us suppose we have a sort function. One way of specifying it is to say that a sort function is any function where if the input/output are vectors $I, O$, then $O_i \leq O_j \forall i < j$ and ...
• 1,311
1 vote
34 views

### Non Turing-Complete Models, Conditional-Complete function?

I know well the distinction between the class of Partial Recursive Functions, and $\mu$-Recursive, i.e. the latter is Turing Complete and the former is equivalent to the LOOP-Program model of ...
1 vote
57 views

### How to justify this causally consistent execution in the $(vis, ar)$ framework for distributed consistency models?

In Figure 5.1 of the book "Principles of Eventual Consistency" by Sebastin Burckhardt, 2014, Causal Consistency (CC); wiki is (mainly) defined as the conjunction of $hb \subseteq vis$ and \$hb \...
• 2,329
1 vote
112 views

### Confusion about the visibility and arbitration relations in a formal framework for distributed consistency models

In the POPL'14 paper "Replicated Data Types: Specification, Verification, Optimality" and the book "Principles of Eventual Consistency", the authors propose a formal framework for ...
• 2,329
1 vote
111 views

### Object-Oriented Programming Languages based on assignment

Is it correct to claim that an object-oriented programming language based on assignment (e.g., Java and Smalltalk) introduces mutability and hence complexity in concurrent applications ? In other ...
• 111
65 views

### Has there already been research done on how data(e.g. runtime) can improve the development environment of a language?

tl;dr; I am being offered a graduate thesis about how to use data about a languages runtime/static analysis of dependencies etc. and feed it back into the development process. And my question is: Has ...
• 125
112 views

### Programming languages with constraints on values of variables?

Hi Theoretical Computer Science Stack Exchange, I have been wondering if there are programming languages where one can have constraints on values variables can have? Have such approach been used in ...
172 views

### Is BigInteger-based Brainfuck Turing Complete?

All of the proofs of Turing-Completeness I've found for Brainfuck rely on its cells being fixed-width integers that wrap around upon over/underflow. The "parent language" P'' on which ...
• 119