Gentzen and computer science

Question

I would like to learn a bit about the connections between Gentzen's discoveries in the 30's related to proof theory and, in particular, his sequent calculus, and the later development of computer languages. Could anyone elaborate a bit on that? I am particularly interested in knowning whether one can find in Gentzen some predecessor of a pointer to a memory address. If so, in which specific form?

Thanks in advance.

Answer 1

According to your previous comments it seems that you already know about the Curry-Howard isomorphism and the Lambda Calculus but I still wrote a general answer to fit the original question.

I don't think I perfectly provided what you want but I hope it can lead to what you're looking for.

Curry-Howard The main link between Gentzen discoveries and Computer Science is the Curry-Howard isomorphism.

It tells us that we have a deep relation between mathematical proofs and computer programs. If you scroll down on the Wikipedia page, you can see several tables with some correspondences. The role of Gentzen's works is fundamental :

• Programs using the cut rule behaves like programs we can evaluate
• Proofs without cuts are similar to programs in normal form (fully evaluated)
• The cut elimination theorem actually behaves like the execution of programs

Note that by "program" we usually mean Functional programs in the context of Curry-Howard.

Linear Logic Gentzen's works led to a very large number of new fields (especially in Computer Science). For instance, Jean-Yves Girard invented/discovered Linear Logic which you can get from the classical sequent calculus by restricting the structural rules. Moreover, Linear Logic handles cut elimination in an amazing way.

Categorical Grammars If you're interested in Linguistics there're also some interesting applications I don't really know/understand. For instance the Lambek Calculus which is related to Lambda-Calculus and Linear Logic.

Ludics Ludics is a quite new and almost unknown formalism suggested by Girard where Logic is founded on some ideas coming from Gentzen (pioneer ideas on Game Semantics), Linear Logic and a philosophy of interaction. Suprisingly, it seems to be connected to linguistics. You may be interested in the works of Alain Lecomte, Myriam Quatrini, Samuel Tronçon, Marie-Renée Fleury. See for instance this and this. He also wrote a whole book on Ludics and Linguistics called "Meaning, Logic and Ludics". I don't know yet if it's related to memory adresses but Ludics has an idea of "location" and "addresses".

Some references I can suggest :

• Starting with Wikipedia pages seems fine to me (Lambda-calculus, Curry-Howard isomorphism)
• The links provided above
• "Proof and Types" (Chapter 2,3,5 but maybe not as a first reading and last part B if you want to know more about Linear Logic), Jean-Yves Girard
• "Lecture notes on the Lambda Calculus" (Chapter 6), Peter Selinger
• "Linear Logic : its syntax and semantics", Jean-Yves Girard