Martin Berger
  • Member for 11 years, 4 months
  • Last seen this week
What is the contribution of lambda calculus to the field of theory of computation?
Accepted answer
103 votes

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

View answer
P and NP classes explanation through lambda-calculus
44 votes

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

View answer
Applicability of Church-Turing thesis to interactive models of computation
37 votes

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

View answer
Books on programming language semantics
34 votes

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

View answer
What's the difference between term rewriting and pattern matching?
Accepted answer
26 votes

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

View answer
Research and open challenges in Programming Language Theory
Accepted answer
26 votes

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

View answer
Why was there a need for Martin-Löf to create intuitionistic type theory?
Accepted answer
24 votes

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

View answer
Why is Proof Checker required in Proof Carrying Code
Accepted answer
19 votes

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

View answer
(How) can you model broadcasts in the pi-calculus?
Accepted answer
19 votes

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

View answer
What constitutes denotational semantics?
19 votes

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

View answer
Historical reasons for adoption of Turing Machine as primary model of computation.
19 votes

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

View answer
How important is knowing how to program for TCS?
17 votes

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

View answer
Is it a Known Concept to Compute an Algorithm Once and Re-Interpret Answer for Different Inputs
Accepted answer
17 votes

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

View answer
Math talk: Theorem about git revision control system?
17 votes

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

View answer
Lipton's most influential results
17 votes

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

View answer
Equivalent formulation of complexity theory in Lambda Calculus?
Accepted answer
16 votes

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

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

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

View answer
Program reasoning about own source code
Accepted answer
15 votes

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

View answer
Algebra oriented branch of theoretical computer science
15 votes

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

View answer
Humanifying computer-generated or computer assisted proofs
13 votes

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

View answer
Are there any annotated formal verification systems for pure functional programming languages?
Accepted answer
13 votes

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

View answer
How can I prove formally semantic equivalence of programming languages?
Accepted answer
13 votes

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

View answer
Is there a theory that combines category theory/abstract algebra and computational complexity?
12 votes

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

View answer
Are there any topics in theoretical CS that are more about pure math?
12 votes

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

View answer
Logical framework vs type theory
Accepted answer
12 votes

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

View answer
Good books on parser theory?
Accepted answer
12 votes

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

View answer
Abstract algebra for Theoretical Computer Scientists
12 votes

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

View answer
What is the intuition behind linear logic?
Accepted answer
11 votes

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

View answer
What functions can System F not compute?
11 votes

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

View answer
"Correctness" of type theory
Accepted answer
11 votes

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

View answer