# Questions tagged [pl.programming-languages]

Programming languages, in particular, focussing on their semantics.

372 questions
Filter by
Sorted by
Tagged with
69 views

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

Suppose $\varphi(x,S)$ is a positive elementary formula, i.e., a first-order formula with second-order relation variable $S$, such that the arity of $x$ and $S$ agree. In this setting, $\varphi$ can ...
71 views

### Generating grammar from a string

Given a string generated with a valid grammar, how can I find list of all the valid grammar for that particular string? Problem statement - I'm trying to build a code base scanner, and I'd like to ...
187 views

### Can you regain the Church-Rosser property in languages with continuations?

I'm aware that if you naively add continuations to a language, the Church-Rosser property no longer holds. For example, suppose we have some variant of the STLC with basic arithmetic and integer types....
67 views

### Is Linear Evaluation Parametric?

Parametric functions satisfy free theorems which state that they take related arguments to related results. This is formalized by the notion of parametric transformation introduced in section 5 of ...
1 vote
200 views

### Is data structure necessarily a functor?

The justification of my conjecture is that (seemly) any data structure can have a mapper that applies a given function $f$ to each element of the structure. A data structure in the end is a container ...
2k views

### Where is the model theory in programming language theory?

I have a background in mathematical logic and am trying to learn some programming language theory. In the syntax of, say, first-order logic, one of the first distinctions you learn about is between ...
115 views

### Formal differences between emulation and simulation?

Recently this question came up, and I've been unable to find a concrete answer. When I was reading this paper on CRDTs, I was a little perplexed by the notion of emulation here in theorems 3.1 and 3.2....
67 views

1 vote
86 views

### Extension of primitive recursion, that is as powerful as System-T

I know that System-T restricted to first-order types is exactly as powerful as primitive recursive functions, because I proved it in Agda. I asked myself, if there is a extension of primitive ...
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 ...
64 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 ...
135 views

### Is there a relation between the techniques used by Dan Willard, versus those of Brown and Palsberg, to exclude diagonalization?

This question extends my inquiry from a previous post . Dan Willard's Self-Justifying Axiom Systems/Self-Verifying Theories  and Brown and Palsberg's self-interpreter for F-Omega  both employ ...
93 views

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

Brown and Palsberg  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 ...
375 views

### Similarities and differences between Pie and popular languages with dependent types

The book The Little Typer explains dependent types using a toy language called Pie (https://github.com/the-little-typer/pie). How similar is Pie to the popular languages with dependent types: Coq, ...
106 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 ...
171 views

### Intuitive way to handle variable binding

Suppose we have an algebraic datatype parameterised by a type variable name, e.g. ...
739 views

### What's the logical counterpart to jumps with arguments on CPS terms?

It's well known that the CPS (continuation-passing style) translation often employed in compilers corresponds to double negation translation under the Curry-Howard isomorphism. Though often the target ...
135 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. ...
184 views

### Is Barbara Liskov's claim that CLU was the first implemented language to provide linguistic support for data abstraction accurate?

According to this paper by Barbara Liskov, CLU was "The first implemented programming language to provide direct linguistic support for data abstraction". She then defines "data ...
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-...
1k views

### How does type theory change how one thinks about programming?

I have been dabbling in HoTT and I am convinced that dependent type theory is much more suitable than set theory for proof assistants. Now, this made me wonder - how fundamental is Type Theory ...
162 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 ...
167 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 ...
73 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 ...
211 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 ...
113 views

### Resource for Understanding this Notation [closed]

I am trying to read this paper: https://arxiv.org/abs/1510.00925. I am familiar with grammars, but I cannot understand the notations in figure 1. Can anyone suggest a resource or book where I can ...
248 views

### What are the pros and cons for type cases in dependent type theories?

Pattern matching on $\cal U$ is allowed in XTT and Idris2 (for unerased types), and that implies the injectivity of type constructors (that's just my intuition, though -- I also wonder how do I prove ...
151 views

### What does x.y notation mean?

In Harper's PFPL (Ed. 2, top of page 8), this notation is used but I don't see a definition. What does $x.y$ mean?
291 views

### Density of semantics in syntax

Let $L$ be a programming language, and $\cong$ a notion of equality of $L$-programs (in general $\cong$ will be undecidable). Let $syntax(n)$ be the number of $L$-programs of size $n$ (for some ...
296 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) ...
526 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 ...
291 views

### Is this variant of bitwise cyclic tag Turing-complete?

Cross-posted to MathOverflow. CT is an extremely minimalist programming language that can simulate arbitrary tag systems, and is therefore Turing-complete. A program consists simply of a string of 3 ...
78 views

### Is there a list of notations developed for regular expressions? [closed]

There is, of course, PCRE. I know also of Olin Shiver's Structural Regular Expressions, and Rob Pike's Structural Regular Expressions. I also understand that Raku's regexps are different from perl's ...
321 views

### Intuition behind nested positivity and counterexamples

I'm looking at the nested positivity conditions for inductive types stated in the Coq manual. First off, are there any other references (not necessarily for Coq, but in dependent type theories ...
1 vote
205 views

### Can concurrency models be compared in terms of some metrics?

In Seven Concurrency Models in Seven Weeks by Butcher, it compares Actor Model and Communicating Sequential Processes (CSP): CSP is more flexible than actor model: In actor model, the medium of ...
171 views

### What graphs on $\mathbb{N}$ can be encoded as regular languages?

Suppose I represent the natural number 0 by "x", and use the symbol "s" for successor so that I get the following encoding of $\alpha : \mathbb{N} \rightarrow V$ of natural numbers ...
83 views

### Nominal Tree Languages i.e. with Binders and Infinite Symbols?

I'm wondering if there has been any research done into automata that accept languages of trees that can bind arbitrary variables, and are considered equal under alpha equivalence. I've found so far: ...
142 views

### Phonology and lambda calculus

I wonder whether there is any relationship between lambda calculus and phonology (study of phonemes). Specifically, how one would use the concepts of lambda calculus (typed or untyped) in the study of ...
1 vote
116 views

### λProlog vs HiLog

λProlog is a well-known higher-order logic programming language. On the other hand, HiLog is described as a logic programming language with higher-order syntax, but first-order model theory. Do I ...
98 views

### Reference request: pi-calculus with simultaneous events

I am interested in using the $\pi$-calculus as a basis for modeling workflows, and came up with an extension that proved useful in my modeling, namely the ability to specify that two or more channel ...
1 vote
205 views

### What relations and differences are between formal semantics for linguistics and for programming languages?

I browsed the table of content of Cann's Formal Semantics, which reminds me of the things that I saw in programming language books. Cann's book is for linguistics, and am I right that it is helpful ...
324 views

### Does the Hindley-Milner type system (i.e. STLC with prenex polymorphism) have a category-theoretic model?

It is well known that any CCC (cartesian closed category) is a model of the simply-typed $\lambda$-calculus. It is less well known that System F admits a categorical model, but it is also well studied ...
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 ...