Questions tagged [pl.programming-languages]

Programming languages, in particular, focussing on their semantics.

Filter by
Sorted by
Tagged with
5
votes
2answers
207 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 ...
-3
votes
0answers
89 views

Do these examples belong to syntax or semantics and are they handled by syntactic or semantic analysis?

In the dragon book 4.3.5 Non-Context-Free Language Constructs A few syntactic constructs found in typical programming languages cannot be speci ed using grammars alone. Here, we consider two of these ...
1
vote
2answers
117 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
135 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
30 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
94 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
88 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
80 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
123 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
184 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
182 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
31 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
192 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 ...
0
votes
0answers
62 views

Sample Terms in System Omega

I've been implementing mini languages that fall into each corner of the Lambda Cube. My main reference for this has been Types and Programming Languages. The latest one I finished is System Omega. I ...
3
votes
0answers
138 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
136 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
69 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
63 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
306 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 ...
5
votes
1answer
147 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
123 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
530 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
214 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
72 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 ...
10
votes
2answers
343 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
48 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
301 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
65 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 ...
6
votes
1answer
342 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
99 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
265 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
369 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
249 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
360 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
108 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
565 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
237 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 ...
11
votes
5answers
450 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
195 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
349 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
142 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, ...
8
votes
1answer
80 views

Question on subtyping of handlers in “An Effect System for Algebraic Effects and Handlers”

I had a question on subtyping in the paper "An Effect System for Algebraic Effects and Handlers". I was wondering why there isn't a subtyping rule for adding effects on both sides of a handler type, ...
3
votes
1answer
124 views

Escaping references in Eff and resources

In the paper "Programming with Algebraic Effects and Handlers" there is the issue where references (dynamic instances of a state effect, defined using algebraic effects) can propagate outside the ...

1
2 3 4 5
7