$\lambda$-calculus has two key roles. It is a simple mathematical foundation of sequential, functional, higher-order computational behaviour. It is a representation of proofs in constructive logic. ...

Turing-machines and $\lambda$-calculus are equivalent only w.r.t. the functions $\mathbb{N} \rightarrow \mathbb{N}$ they can define. From the point of view of computational complexity they seem to ...

I think the issue is quite simple. All interactive formalisms can be simulated by Turing machines. TMs are inconvenient languages for research on interactive computation (in most cases) because ...

It all depends how deep you want to go, and how much you already know. For a beginner Winksel's book is really nice, but yes, it's not introducing you to the state of the art in semantics as it was ...

One way of looking at these two concepts is to say that pattern matching is a feature of programming languages for combining discrimination on constructors and destructing terms (while at the same ...

I think the overall goal of PL theory is to lower the cost of large-scale programming by way of improving programming languages and the techincal ecosystem wherein languages are used. Here are some ...

Very briefly: the simply-typed $\lambda$-calculus does not have dependent types. Dependent types were proposed by de Bruijn and Howard who wanted to extend the Curry-Howard correspondence from ...

The purpose of the proof checker is to minimise the trusted computing base. By having a proof checker, neither the compiler nor the theorem prover need to be correct. The paper makes this point on ...

About a decade ago, Ene and Muntean showed that broadcasting has no reasonable compositional encoding into the $\pi$-calculus [1]. The essence of their separation between point-to-point communication ...

I agree that A. Bauer's identification of denotational semantics with compositionality (in Books on programming language semantics) doesn't really characterise well what has traditionally been meant ...

I would like to weaken the claim that TMs are the primary model of computation, or at least point towards another dimension of the question. Clearly TMs are dominant in the more complexity- and ...

Thank you Gopi for this question. I'd like to extend the many interesting answers in another dimension that hasn't been mentioned yet. Research is not the only thing we do at university: if you want ...

I'm not sure, but you might be talking about what has been termed incremental computation. The key idea behind incremental computation is to program in a way such that the program responds to input ...

Interestingly, there is a nascent mathematisation of version control systems, although at this point it's only partially applicable to Git. It's called patch theory [1, 2, 3, 4, 5] and arose in the ...

I'm not 100% sure if the explanation below is historically accurate. If it isn't, please feel free to edit or remove. Mutation testing was invented by Lipton. Mutation testing can be seen as a way to ...

As you point out, the λ-calculus has a seemingly simple notion of time-complexity: just count the number of β-reduction steps. Unfortunately, things are not simple. We should ask: Is counting β-...

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 ...

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 ...

Your knowledge of field theory would be useful in cryptography, while category theory is heavily used in the research on programming languages and typing systems, both of which are closely related to ...

You are probably thinking of Gower's work with Ganesalingam, based on the latter's MSc dissertation (1). Gowers blogged about this in (2) and other places, and they've written a paper on the subject (...

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 ...

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 ...

[Computational complexity and category theory] seem like such natural pairs. Given the prominence of computational complexity as a research field, if they were such natural bedfellows, maybe somebody ...

Here are three more fields that fit your criteria. Category theory. This is clearly interesting to most pure maths fields, but also has been very influential in the theory of (functional, sequential) ...

Summary. A logical framework is a meta-language for the formalisation of deductive systems, where deductions become syntactic objects. Of course what counts as a meta-language is quite vague, and it ...

One book that I can recommend is D. Grune, C. J. H. Jacobs, Parsing Techniques: a Practical Guide.

One possibily path into abstract algebra could be to look at it from point of view of cryptography, which is about algorithms on finite field. Fields are rings, and fields are also two groups coupled ...

I'm not sure this question is ideal for CSTheory, but given that it's already gathering upvotes, here is an answer somebody might have given had the question been posted on cs.stackexchange. In ...

It is somewhat misleading to say that Haskell's typing system is "the hinley-milner type system". Haskell's types are much more powerful, including, among others, higher-kinded types. Indeed the ...

Type theories have multiple uses, and with each kind of usage comes a different notion of correctness. They two key uses are As a foundation of mathematics. In this context correctness means ...