2022 Developer Survey is open! Take survey.
36 votes
Accepted

What are some good introductory books on type theory?

Software Foundations by Benjamin C. Pierce would be a good place to start. It would be a make a good precursor to his Types and Programming Languages. There is also Simon Thompson's Type Theory and ...
user avatar
22 votes

Using lambda calculus to derive time complexity?

A recent developpement on this topic: U. dal Lago and B. Accatoli proved that the length of the leftmost-outermost reduction (LOr) of a $\lambda$-term is an invariant (time) cost model for $\lambda$-...
user avatar
  • 676
21 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 ...
user avatar
20 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 ...
user avatar
17 votes

Status quo of category theory and monads in theoretical computer science research?

There have been a number of developments with regards to the use of monads in the theory of computation since Eugenio Moggi's work. I am not able to give a comprehensive account, but here are some ...
user avatar
  • 26.4k
16 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 ...
user avatar
15 votes

Are there any annotated formal verification systems for pure functional programming languages?

You might want to check out Liquid Haskell, which allow working with type refinements rather than dependent types. Type refinements can be seen as a restricted logical language that allow you to ...
user avatar
  • 13.1k
15 votes
Accepted

Scott's stochastic lambda calculi

One apparent strength of his approach is that it allows higher-order functions (i.e. lambda terms) to be observable outcomes, which measure theory generally makes quite tricky. (The basic problem is ...
user avatar
15 votes
Accepted

Program reasoning about own source code

I think you are asking about two different things. The ability of a programming language to represent all its programs as data. Reasoning about programs as data. For analytical purposes it's ...
user avatar
14 votes
Accepted

Algorithm to determine function equality on the simply typed lambda calculus?

As I said in my comment, the answer in general is no. The important point to understand (I say this for Viclib, who seems to be learning about these things) is that having a programming language/set ...
user avatar
14 votes
Accepted

Can we distinguish strictly syntactic and semantic methods in programming language?

No, you cannot strictly distinguish syntactic from semantic methods, but the distinction still ends up making sense. Structural operational semantics is not denotational, because it is not a ...
user avatar
14 votes
Accepted

Is this behavior in a programming language inconsistent?

Yes, your type inference seems incomplete. This example can be dealt with fairly trivially, by computing the respective type equations, e.g. in the style Hindley/Milner does it. Alpha-renaming the ...
user avatar
14 votes
Accepted

Logical Reations for an Impredicative System in a Predicative MetaTheory

In general, what we usually call the logical relations argument isn't really linked to impredicativity: the main idea is simply to interpret terms in some abstract algebra $\cal A$, and to represent ...
user avatar
  • 13.1k
13 votes
Accepted

How can I prove formally semantic equivalence of programming languages?

Comparing two programming languages is difficult is a difficult problem, and far from being solved. The key issue is that there are many different ways languages can be compared, and none of them is ...
user avatar
13 votes
Accepted

Are there any annotated formal verification systems for pure functional programming languages?

Honda and Yoshida's A Compositional Program Logic for Polymorphic Higher-Order Functions (probably) pioneered Hoare logics for purely functional languages. This work is based on Hennessy-Milner ...
user avatar
12 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 ...
user avatar
  • 26.4k
11 votes

What's the relation between OOP and category theory?

There are absolutely some relationships between the semantics and practice of OOP and category theory. This is somewhat unsurprising since both fields attempt to give a principled generic account of ...
user avatar
  • 13.1k
11 votes

What are some good introductory books on type theory?

Barendregts Lambda Calculi with Types is more advanced, but it covers some important topics in the "classical" theory of types.
user avatar
  • 13.1k
11 votes

Are there any annotated formal verification systems for pure functional programming languages?

See also Yann Régis-Gianas PhD thesis work with François Pottier: A Hoare Logic for Call-by-Value Functional Programs (MPC'08). This work was extended to cover the usual ML side-effects by Johannes ...
user avatar
  • 1,882
11 votes
Accepted

Reference for the fact that (0=1) implies false requires a universe in MLTT

I know of: Jan M. Smith, The independence of Peano's fourth axiom from Martin-Löf's type theory without universes, The Journal of Symbolic Logic 53(3), p. 840-845, 1988.
user avatar
11 votes

An example where smallest normal lambda term is not fastest

Blum’s speedup theorem is usually stated in the language of partially recursive functions, but up to trivial differences in notation, it works just the same in the language of $\lambda$-calculus. It ...
user avatar
11 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 ...
user avatar
11 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 ...
user avatar
  • 16.6k
11 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 ...
user avatar
  • 1,882
11 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, ...
user avatar
11 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, ...
user avatar
10 votes
Accepted

Program Minimization

There is a naive algorithm for programs with bounded-size inputs: enumerate all programs in order of increasing length (or execution time, which is a bounded function of the length). If you can prove ...
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 ...
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 ...
user avatar
  • 1,147
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$ (...
user avatar
  • 26.4k

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