Questions tagged [pl.programming-languages]

Programming languages, in particular, focussing on their semantics.

Filter by
Sorted by
Tagged with
4
votes
2answers
243 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 ...
2
votes
0answers
209 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) ...
0
votes
0answers
123 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 ...
4
votes
1answer
135 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 ...
2
votes
0answers
65 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 ...
6
votes
2answers
234 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
2answers
134 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 ...
2
votes
1answer
140 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 ...
1
vote
0answers
33 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: ...
1
vote
1answer
97 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
0answers
91 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 ...
3
votes
1answer
83 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
1answer
143 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 ...
7
votes
2answers
199 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 ...
3
votes
1answer
193 views

Why would the term “dynamically typed” be considered a misnomer?

In the book "Types and Programming Languages", the author writes: The word "static" is sometimes added explicitly - we speak of a "statically typed programming language",...
1
vote
0answers
32 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 ...
4
votes
1answer
224 views

Areas of research and open problems in functional programming [closed]

What are the major areas of functional programming that require more research and development? For example, I know a lot of people are asking for dependent types in Haskell, and someone at my uni is ...
3
votes
0answers
143 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
votes
0answers
107 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\...
1
vote
1answer
141 views

Lack of atomic propositions in the Calculus of Constructions from ATTAPL textbook

I am working through the Dependent Types chapter from Advanced Topics in Types and Programming Languages (ATTAPL) by Benjamin Pierce et al. I am confused with the calculus presented Fig 2-7 (Calculus ...
0
votes
0answers
76 views

Proposition terms vs types in Coq

Consider the following div function written in Coq. It takes in a proof that the divider is non-zero. Definition div (n d:nat) (pf: ~(d = 0)) := n/d. Focus on <...
-1
votes
1answer
65 views

Chomsky-Schutzenberg Hierarchies explained for physicist (general) [closed]

I am classically trained in physics, however I have been interested in the use of information theory in studying some classical systems. As someone who is somewhat unfamiliar with the language of ...
7
votes
3answers
328 views

Can Non-termination be considered an algebraic effect?

Non-termination is sometimes considered an effect. I have been reading about algebraic effect systems (What is algebraic about algebraic effects and handlers?), and I suspect non-termination (like ...
6
votes
1answer
149 views

Conservative Approximation of Kleene-Mycroft Iteration for Polymorphic Recursion?

To perform type inference in the presence of polymorphic recursion, one can use a Kleene-Mycroft iteration to compute the principal type of an expression. To type $\mathsf{fix}\ f\ldotp e$, we define $...
3
votes
1answer
129 views

Verified type checkers

Most of the work on programming language metatheory mechanization focus on the declarative properties of the languages (e.g., type soundness), but fail to address the algorithmic side, i.e. the type ...
9
votes
2answers
596 views

Applications of algebraic geometry in type theory/programming language theory

Lately, I have become interested in algebraic geometry and have started reading on it. I still know very little about this field, but I do want to know if it has any connection with my main field, ...
0
votes
1answer
223 views

Where does a C-like language without heaps belong in the automata hierarchy?

Assume that the language C', unlike C, has well-defined semantics, but has similar features: pointers and manual memory management through malloc and free. Assume that C'' is the same as C' without ...
11
votes
1answer
1k views

What is the “question” that programming language theory is trying to answer?

I've been interested in various topics like Combinatory Logic, Lambda Calculus, Functional Programming for a while and have been studying them. However, unlike the "Theory of Computation" which ...
0
votes
0answers
76 views

How to get started with program synthesis

I am a CS Major, I am a programmer with 10 years of experience. i want to get to know about program synthesis. there are no video tutorials / courses available online. i have researched about Emina ...
11
votes
2answers
400 views

Intuition Behind Strict Positivity?

I'm wondering if someone can give me the intuition behind why strict positivity of inductive data types guarantees strong normalization. To be clear, I see how having negative occurrences leads to ...
1
vote
0answers
50 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 \...
3
votes
2answers
348 views

Extending Hindley-Milner to type mutable references

I have been trying to implement a programming language from scratch, and have gotten reasonably far. It reads just like Python, other than the fact that let is used ...
1
vote
0answers
70 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 ...
7
votes
1answer
378 views

How to tell if an effect is algebraic?

I've read Bauer's What is algebraic about algebraic effects and handlers? and he talks about IO being an algebraic effect, even though it doesn't have any equations. In other papers on algebraic ...
4
votes
0answers
101 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 ...
5
votes
1answer
191 views

Is F<: with bottom undecidable?

We all know that F<: is undecidable: http://www.cse.chalmers.se/~abela/lehre/SS07/Typen/pierce93bounded.pdf However, I have difficulties finding that anyone claiming the version with bottom added ...
4
votes
0answers
143 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 ...
3
votes
1answer
272 views

Busy Beaver Equivalent for the Untyped Lambda Calculus

In the same way that the Busy Beaver function is defined for Turing Machines, we could define a similar function for the untyped lambda calculus: Over all terms in the ULC composed of ...
11
votes
2answers
374 views

Hereditary substitution with a universe hierarchy

I've read about hereditary substitution for the Simple Lambda Calculus and for The Logical Framework with distinct terms and types. I'm wondering, are there any examples of hereditary substitution in ...
5
votes
2answers
256 views

Typing of substitution in a bidirectional type system

In most typed lambda calculi, we have the following lemma: If $\Gamma \vdash t_1 : \tau_1$ and $\Gamma, x : \tau_1, \Delta \vdash t_2 : \tau_2$ then $\Gamma,\Delta[t_1/x] \vdash t_2[t_1/x] : \tau_2[...
5
votes
2answers
367 views

Preservation under Substitution with Telescopes

In the simply typed lambda calculus, one can show the following result, known as "preservation under substitution": If $\Gamma \vdash v : \tau_1$ and $(x : \tau_1) \vdash t : \tau_2$, then $\Gamma \...
6
votes
2answers
113 views

Formal semantics of tactics

Tactics are supposed to represent inference rules in a system, and it might seem unnecessary at first to formalize the semantics of tactics; nevertheless, modern theorem provers can have pretty ...
11
votes
1answer
607 views

Proof techniques for showing that dependent type checking is decidable

I'm in a situation where I need to show that typechecking is decidable for a dependently-typed calculus I'm working on. So far, I've been able to prove that the system is strongly normalizing, and ...
6
votes
3answers
257 views

Why/when do we ever need transfinite loop variants?

I do not understand why one would ever need a transfinite loop variant. Why do natural-number-valued variants not suffice? My simple (but perhaps too naive) argument is: if a loop $L$ terminates ...
12
votes
5answers
477 views

Representing bound variables with a function from uses to binders

The problem of representing bound variables in syntax, and in particular that of capture-avoiding substitution, is well-known and has a number of solutions: named variables with alpha-equivalence, de ...
5
votes
1answer
201 views

Confusion about a formal definition of PRAM consistency

I am reading the paper "Consistency in Non-Transactional Distributed Storage Systems" by Paolo Viotti and Marko Vukolić. The authors provide a comprehensive survey of various consistency semantics ...
5
votes
3answers
461 views

Sorting a programs instructions until it works

Lets say I have a computer program below. (define (factorial x) (if (= x 0) 1 (else (* x (factorial (- x 1))))) I then take each line of the ...
-1
votes
1answer
422 views

What is the practical importance of making or using a Turing complete language? [closed]

I get what a Turing machine is and what language is a Turing-complete language but when someone introduces me to a new programming language (like Solidity) and says it is Turing complete, what am I ...
5
votes
2answers
158 views

Does Standard ML validate (CBV) eta equivalence?

$\eta$ equality of functions is fundamental in their Category-theoretic semantics but in practice even "functional" languages include "impure" features that violate it. Note that this is not an issue ...
6
votes
4answers
6k views

Difference between syntax and semantic error in programming languages

When compilers generate errors for a specific programming language, there's distinction between syntax & semantic errors. E.g. ) + f 3 has ill-formed syntax, ...

1
2 3 4 5
7