Skip to main content

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
13 votes
0 answers
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 ...
Neel Krishnaswami's user avatar
11 votes
0 answers
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_{...
Noam Zeilberger's user avatar
10 votes
0 answers
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 ...
gasche's user avatar
  • 2,040
10 votes
0 answers
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 ...
chi's user avatar
  • 678
8 votes
0 answers
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$.&...
Siddharth's user avatar
  • 851
8 votes
0 answers
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 ...
Jake's user avatar
  • 1,203
8 votes
0 answers
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 ...
sclv's user avatar
  • 1,379
7 votes
0 answers
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. ...
PaR's user avatar
  • 71
7 votes
0 answers
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 ...
Neel Krishnaswami's user avatar
7 votes
0 answers
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 ...
MaiaVictor's user avatar
  • 3,157
6 votes
0 answers
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 ...
vigenary's user avatar
6 votes
0 answers
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 ...
Max New's user avatar
  • 1,695
6 votes
0 answers
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 ...
MaiaVictor's user avatar
  • 3,157
6 votes
0 answers
282 views

Generalizing Haskell: could we replace Hask with Cat?

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 ...
Bob's user avatar
  • 381
5 votes
0 answers
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 ...
Siddharth's user avatar
  • 851
5 votes
0 answers
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 ...
numerodix's user avatar
  • 151
5 votes
0 answers
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 ...
Jules's user avatar
  • 390
4 votes
0 answers
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 ...
Gro-Tsen's user avatar
  • 841
4 votes
0 answers
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-...
Ryan Kavanagh's user avatar
4 votes
0 answers
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 ...
Joey Eremondi's user avatar
4 votes
0 answers
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 ...
Joey Eremondi's user avatar
4 votes
0 answers
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 ...
hengxin's user avatar
  • 2,329
3 votes
0 answers
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 ...
jpt4's user avatar
  • 111
3 votes
0 answers
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 ...
Siddharth's user avatar
  • 851
3 votes
0 answers
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 (...
Joey Eremondi's user avatar
3 votes
0 answers
128 views

Equational Theories for Type Systems

I was reading through Gunter's Semantics of Programming Languages: Structure and Techniques and in the second chapter on simply typed $\lambda$ calculus he introduces an equational theory with $\beta\...
Apoorv's user avatar
  • 141
3 votes
0 answers
177 views

How useful is program search in the field of programming-language theory?

I've been thinking: computing systems such as the Lambda Calculus and its variations are usually very simple and can be implemented in as few as ~80 lines of Haskell code. There is a self-interpreter ...
MaiaVictor's user avatar
  • 3,157
3 votes
0 answers
408 views

Is there any system where function equality (extensionality) is decidable?

Is there any programming language or system where function equality (extensionality) is decidable?
MaiaVictor's user avatar
  • 3,157
3 votes
0 answers
216 views

Understanding the goals you can reach with different programming models and languages

I come to ask this question here, because Meta told me this place was probably best for it. Reference: https://meta.stackexchange.com/questions/114043/ I've read this article many a times and ran in ...
Koen027's user avatar
  • 139
2 votes
0 answers
101 views

Is there a relationship between Brown and Palsberg's Self-Interpreter for F-Omega and Lawvere's Fixed Point Theorem?

Brown and Palsberg [0] demonstrated an self-interpreter for F-Omega. To do so, they perform "a careful analysis of the classical theorem [of the impossibility of self-interpretation by total ...
jpt4's user avatar
  • 111
2 votes
0 answers
74 views

Reference request: characterisation of simultaneous substitution

For simply typed λ-calculus, a simultaneous substitution from $\Gamma$ to $\Delta$ is concretely a type-preserving map from variables in $\Delta$ to terms in $\Gamma$. See, for example, Programming ...
mudri's user avatar
  • 121
2 votes
0 answers
309 views

Are CCS and CSP still worth studying?

In Winskel's The formal semantics of programming languages 1993, Ch14 Nondeterminism and parallelism says This chapter is an introduction to nondeterministic and parallel (or concurrent) ...
Tim's user avatar
  • 639
2 votes
0 answers
84 views

Categorical model of binding / first class modules

Binders are explained using presheaves (Pitts/Gabbay A new approach to Abstract Syntax with variable binding) What is the equivalent (categorical) theory to explain first class modules as in 1ML ?
nicolas's user avatar
  • 121
2 votes
0 answers
177 views

Is there is an intuitive explanation why call-by-name PCF is less expressive than both call-by-value PCF and lazy PCF?

J.C. Mitchell cites in his "Expressive power of programming languages" the result in Riecke's "Fully abstract translations between functional languages" about the call-by-value, call-by-name and lazy ...
Akram El-Korashy's user avatar
2 votes
0 answers
106 views

Are the sets of executions of data-race free programs equal, when run on causal memory and on sequentially consistent memory respectively?

In the paper "Causal Memory: Definitions, Implementations, and Programming (Distributed Computing [DC] 1995)", the authors present a formal definition of causal memory, an abstraction of distributed ...
hengxin's user avatar
  • 2,329
2 votes
0 answers
204 views

Evaluation contexts: outside-in vs inside-out

I heard that there exist two styles to define an evaluation context: outside-in and inside-out. Can someone give the definitions? Why are they so named (inside-out and outside-in)? What is the ...
day's user avatar
  • 2,805
2 votes
0 answers
183 views

Recursion Schemes for Static Analysis (AST)

In the process of creating an AST analysis framework one of the challenges is creating good reusable functions and to avoid too much boiler-plate code. To that end catamorphisms seem like a good fit, ...
Bent Rasmussen's user avatar
1 vote
0 answers
54 views

How to Classify Memory Access Pattern by LLVM or Other Tools?

I am currently encountering issues with using LLVM. Here is my specific problem: I want to study the memory access patterns of applications that are suitable for mapping onto a Spatial Accelerator, ...
Chris_Wu's user avatar
1 vote
0 answers
85 views

Abstract domain monad

I was reading old lecture from a CS course at Cornel and I have some doubts about the following at 2.4 It defines how to transform domains between each other via a Galois Insertion, more formally: ...
Alecs's user avatar
  • 11
1 vote
0 answers
78 views

Is it possible to define beta reduction for PHOAS?

I'm using Parametric Higher-Order Abstract Syntax (PHOAS) as a representation for untyped lambda calculus in OCaml: ...
Hirrolot's user avatar
  • 105
1 vote
0 answers
97 views

Alternative notions of bisimulation

Suppose $(S, \Lambda, \rightarrow)$ is a labeled transition system. A bisimulation is a relation $R \subseteq S \times S$ s.t. $\forall \alpha \in \Lambda$ and $\forall p, q \in S$ with $R(p,q)$, $\...
NathanLiitt's user avatar
1 vote
0 answers
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 ...
Opt's user avatar
  • 1,311
1 vote
0 answers
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 ...
Antonio Caruso's user avatar
1 vote
0 answers
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 \...
hengxin's user avatar
  • 2,329
1 vote
0 answers
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 ...
hengxin's user avatar
  • 2,329
1 vote
0 answers
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 ...
Sergio's user avatar
  • 111
0 votes
0 answers
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 ...
DenLilleMand's user avatar
0 votes
0 answers
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 ...
Tomi Pannila's user avatar
0 votes
0 answers
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 ...
user513093's user avatar
0 votes
0 answers
569 views

What is the difference between a model of computation and a programming language?

https://en.wikipedia.org/wiki/Model_of_computation includes sequential models, functional models and concurrency models. Sequential models include finite state machine, Turing machines, random access ...
Tim's user avatar
  • 639