23 votes
Accepted

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

Roughly speaking, there are two main strategies for safe manual memory management. The first approach is to use some substructural logic like linear logic to control resource usage. This idea has ...
Neel Krishnaswami's user avatar
21 votes

Why do functional programming languages require garbage collection?

All of the following comments are premised on the choice of a standard implementation strategy using closures to represent function values and a call-by-value evaluation order: For the pure lambda ...
Neel Krishnaswami's user avatar
18 votes

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

The overall purpose of PLT is to make industrial software engineering (in a general sense) cheaper (also in a general sense), through optimising the most important tool (programming languages) and ...
Martin Berger's user avatar
14 votes
Accepted

Applications of algebraic geometry in type theory/programming language theory

To my knowledge (which is definitely incomplete), there has been relatively little work on this, presumably because it requires assimilating two relatively intricate bodies of knowledge. However, ...
Neel Krishnaswami's user avatar
14 votes

Where is the model theory in programming language theory?

Let me amend Damiano's answer with more specific comments. Terms of type bool are not logical statements. Expressions like ...
Andrej Bauer's user avatar
  • 28.9k
13 votes

Why/when do we ever need transfinite loop variants?

You are correct when you observe that for any particular terminating loop $L$ we may simply define the invariant "we're getting one step closer to termination". But proving that this is indeed a valid ...
Andrej Bauer's user avatar
  • 28.9k
13 votes
Accepted

Where is the model theory in programming language theory?

The model theory of programming languages is called denotational semantics. You can google the term to find out more about it, I'll give an extreme synthesis of it. Denotational semantics is a ...
Damiano Mazza's user avatar
12 votes
Accepted

A bicartesian closed category of strict complete partial orders (Hask)

Yes, it's impossible to have a nondegenerate CCC with general recursion and categorical coproducts. The standard reference for this is: H. Huwig and A. Poigne. A note on inconsistencies caused by ...
Neel Krishnaswami's user avatar
12 votes
Accepted

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

From a programming language theory perspective, as opposed to the computability perspective other answers and comments have offered, C++ templates combined with concepts correspond to bounded ...
Dave Clarke's user avatar
  • 16.7k
12 votes

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

No, to my knowledge there has been no work on formalizing TeX of the kind you are interested in. (What follows is a subjective and personal commentary). I think it is an intriguing and well-posed ...
gasche's user avatar
  • 2,040
12 votes

Representing bound variables with a function from uses to binders

Andrej's and Łukasz's answers make good points, but I wanted to add additional comments. To echo what Damiano said, this way of representing binding using pointers is the one suggested by proof-nets, ...
Noam Zeilberger's user avatar
10 votes
Accepted

Why is the multi-step reduction of semantics reflexive?

The practical reason is that it is very convenient to include also the case "zero steps" in the definition of "many steps" (millennia of mathematical experience have taught us that it is usually a ...
Damiano Mazza's user avatar
10 votes

Representing bound variables with a function from uses to binders

I'm not sure how your variable-to-binder-function would be represented and for what purpose you'd like to use it. If you are using back-pointers then as Andrej noted the computational complexity of ...
Łukasz Lew's user avatar
  • 1,187
10 votes

Preservation under Substitution with Telescopes

The most general form of substitution theorems speaks about arbitrary contexts: Define what it means to have a substitution $\sigma : \Gamma \to \Delta$ from a context $\Gamma$ to a context $\Delta$ (...
Andrej Bauer's user avatar
  • 28.9k
10 votes
Accepted

How to tell if an effect is algebraic?

The general answer which you do not want to hear is: an effect is algebraic if it can be described using operations and equations. The question is a bit open-ended and gives no hint as to what you're ...
Andrej Bauer's user avatar
  • 28.9k
10 votes
Accepted

Similarities and differences between Pie and popular languages with dependent types

I'd say that Pie is a much smaller version of the core languages of those systems. It's a bit closer to Lean's core than to Coq, Agda, or Idris, but the differences are not very large there. When I ...
David Christiansen's user avatar
9 votes
Accepted

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

(With apologies for a long answer that goes in a direction different from the scope of the site: frankly I was surprised to see the question here in the first place….) TeX was designed for ...
ShreevatsaR's user avatar
9 votes
Accepted

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

I'm surprised we don't get this question more often, for Andrej and I have considered adding this rule for quite some time and believed to have proven its correctness. But in the end, it turned out to ...
Matija Pretnar's user avatar
9 votes

Why/when do we ever need transfinite loop variants?

I would like to add the following to Andrej's response (not enough rep for a comment). Indeed, we cannot avoid ordinals but we may hide them. One approach is to use some modal logic that takes ...
Henning Basold's user avatar
9 votes
Accepted

Proof techniques for showing that dependent type checking is decidable

There is indeed a subtlety here, though things work out nicely in the case of type checking. I'll write down the issue here, since it seems to come up in many related threads, and try to explain why ...
cody's user avatar
  • 13.9k
9 votes

Hereditary substitution with a universe hierarchy

As of November 2018, how to do this for dependent type theories with large eliminations is an open question. Establishing that the recursion is well-founded is not too bad; you can use Pataraia's ...
Neel Krishnaswami's user avatar
9 votes
Accepted

Extending Hindley-Milner to type mutable references

To get behaviour similar to Ocaml, simply avoid generalizing the type of mutable variables. With ordinary let-bindings, you generalize if you bind a value, and don't generalize otherwise. With ...
Neel Krishnaswami's user avatar
9 votes
Accepted

Intuition Behind Strict Positivity?

It sounds like you want an overview of normalization arguments for type systems with positive datatypes. I'd recommend Nax Mendler's PhD dissertation: http://www.nuprl.org/documents/Mendler/...
cody's user avatar
  • 13.9k
8 votes

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

I thought a bit about this and I am afraid that it is harder than it looks -- as you suspected! In the spirit of encouraging discussion, I'll write my chain of thoughts. The subtyping rules are often ...
gasche's user avatar
  • 2,040
8 votes
Accepted

Do we care about confluence because of unique normal forms?

I don't know what you mean by "practical", but confluence is very useful from the semantic point of view. Hopefully other people will be able to give you other answers from other points of view (for ...
Damiano Mazza's user avatar
8 votes
Accepted

List of (unsolved) complexity problems arising from PL

Pippenger's (1) from 1996 shows that (under some assumptions) strict (CBV) functional programming languages are asympotically slower than imperative languages. It is open whether Pippenger's result ...
Martin Berger's user avatar
8 votes

Formal semantics of tactics

Obviously there is an operational semantics of Ltac by Jedynak et al.
xrq's user avatar
  • 1,175
8 votes
Accepted

Formal semantics of tactics

I'm not sure this answers your question, but the first (?) paper on the subject of tactics appears to have been Milner's The Use of Machines to Assist in Rigorous Proof.
Martin Berger's user avatar
8 votes
Accepted

Preservation under Substitution with Telescopes

The property, which I would call "typing of substitution" should hold in any type theory, and is not dependent on the exchange property (which I assume is what you mean by permutation) The key is ...
Max New's user avatar
  • 1,675
8 votes
Accepted

Hereditary substitution with a universe hierarchy

Here's a reference for predicative System F. The measure indeed includes the multiset of universe levels in a type. I can't say much about whether this approach generalizes to predicative dependent ...
András Kovács's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible