Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [pl.programming-languages]

Programming languages, in particular, focussing on their semantics.

2
votes
1answer
80 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 ...
8
votes
2answers
220 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
0answers
114 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 ...
9
votes
1answer
506 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
57 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 ...
9
votes
2answers
177 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
41 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
177 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
59 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 specifying ...
5
votes
1answer
199 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
76 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
183 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
128 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
0answers
122 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 ...
10
votes
2answers
303 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
181 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
311 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 \...
5
votes
2answers
94 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 ...
10
votes
1answer
427 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
205 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
365 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
177 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
450 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
115 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
110 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 ...
5
votes
3answers
2k 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
60 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
103 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 ...
7
votes
1answer
228 views

Avoiding Cycles with Unification and Subtyping

Context I realize that subtyping often doesn't admit principle types, and that inference in the presence of subtypes is undecidable. I'm working in a context where typechecking should simply fail ...
2
votes
1answer
158 views

programming language with type-level functions

Is there any programming language out there that allows the same set of tools it offers, to be used at the type level as well? I know, Haskell and some other ML family languages allow parametric types ...
20
votes
2answers
2k views

Has the semantics of TeX (as a programming language) ever been formalized?

It seems to me that the macro language employed by $\TeX$ can maybe be seen as some kind of term rewriting system or some kind of programming language with call-by-name scoping. Even modern ...
17
votes
1answer
321 views

List of (unsolved) complexity problems arising from PL

What are some major, open computational complexity problems that arise from programming languages, especially program analysis and compilation? I am looking for problems on the lines of "the time ...
0
votes
1answer
110 views

Language/type system closest to Haskell without general recursion

I've implemented a completely functional DSL, and now I'd like to reason about it. It would be helpful to be able to compare it to existing languages. The type system is parametric polymorphic with ...
12
votes
3answers
321 views

Type-based memory safety without manual memory manage or runtime garbage collection?

Let's say we wanted a typeful, pure functional programming language, like Haskell or Idris, that is aimed at systems programming without garbage collection and has no runtime (or at least not more ...
2
votes
2answers
155 views

How can you state how abstract interpretation gets around Rice's Theorem succinctly?

At this question, abstract interpretation has a nice in-depth look. However, I'd like someone to clearly and very precisely state how abstract interpretation takes the result of Rice's Theorem over ...
1
vote
1answer
160 views

Algebraic effects and handlers, dynamic effects

What exactly are dynamic effects? What does it mean to dynamically create an effect? In a language with algebraic effects and handlers (such as Eff or Koka) one could already do different operations ...
2
votes
0answers
71 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 ?
1
vote
0answers
97 views

Definitions of strongest postconditions [closed]

The weakest precondition of while loop $\mathtt{while}(G)\{C\}$ with respect to postcondition $P$ can be characterized by the least fixed point of the predicate transformer $X ~\mapsto \neg G \wedge ...
4
votes
1answer
115 views

Questions about algebraic effects and handlers, decomposed handlers

Can a handler always be decomposed? Say a handler for Get and Set effects could be decomposed to a handler for Get and a handler for Set. After they could be composed again by first applying the ...
3
votes
2answers
205 views

Languages that lack contraction, weakening or exchange

When learning about generalized arrows, a question arised to me: Are there any languages (or potential languages) that lack one or more of the structural rules: contraction, weakeing and exchange? ...
2
votes
1answer
108 views

Is there a sense in which we can say error returned from a function is the reverse of context?

This came up in a discussion about golang, but I think it applies more generally. Context in which a function is executed (specially in when we have RPCs) and error returned from a function seem to ...
8
votes
2answers
1k views

What kind of theoretical object corresponds to a C++ concept?

I am lacking a background in theoretical computer science but I would have liked to understand to what kind of theoretical objects C++ concepts corresponds to. Basically, C++ concepts allow to define ...
2
votes
1answer
82 views

Completeness of Constraint Typing (type inference) question regarding $\sigma'$

The theorem of completeness of type inference states the following: Suppose $\Gamma \vdash t:S| _{\mathcal{X}}C$, ...
6
votes
0answers
133 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 ...
6
votes
1answer
168 views

Graph rewriting with one-to-many pattern matching?

In the single-pushout approach to graph rewriting, many nodes in a pattern graph can be matched to a single node of a target graph. My question is if there is a notion of graph rewriting where the ...
7
votes
2answers
132 views

What's the definition of join on iso-recursive types?

In languages with subtyping, there is often a "join" operation defined to compute the least upper bound of two types. It's used in type-checking, for example to find the smallest type that covers both ...
7
votes
2answers
221 views

Efficiently ordering typed programs

Sometimes it is useful to enumerate in increasing order programs that have a given type. A simple example is test generation for compilers: we want to test a new optimising phase and are ...
3
votes
2answers
151 views

Why is the multi-step reduction of semantics reflexive?

I was reading Programming Languages and Lambda Calculi, which defines the multi-step reduction to be the reflexive-transitive closure of the one-step reduction. (Page 15, $\twoheadrightarrow_r$ is the ...
7
votes
1answer
203 views

Do we care about confluence because of unique normal forms?

Confluence implies uniqueness of normal forms, which is great. It is also much simpler to reason about, allowing more reusable proofs (indeed I don't imagine a way to prove UN directly for the $\...
1
vote
1answer
188 views

Can recursion be replaced with a finite set of higher-order functions? [closed]

I am wondering if there is some proof that all recursive algorithms can be rewritten to use some known set of higher-order functions instead of recursion. I'm talking about functions like fold, map, ...