From Turing to Type Theory: The Rich Historical Context of Computation

Pedro Abreu, the host of Type Theory Forall podcast, will talk about the history of computer science leading to the concomitant development of the lambda calculus.

Doors open at 17.30 and the presentation begin at 18:00. Food, refreshments and networking to follow.

Address: Recorded Future's office, 5th floor, Hvitfeldtsplatsen 7, 411 20 Göteborg

Agenda:
17.30 Doors open, food, networking and drinks

18.00 From Turing to Type Theory: The Rich Historical Context of Computation

19:00 - 20:30 Networking

Talk: From Turing to Type Theory: The Rich Historical Context of Computation

We all know that Alan Turing is considered the father of computing for inventing the "Turing Machine" at the young age of 24. But not everyone is aware of how the history of computing is closely tied not only to computers but also to logic and the formal limits of mathematics itself. In this talk, He will delve into the rich historical context behind the invention of the Universal Turing Machine, Hilbert's Problems, Gödel's Incompleteness Theorems, Tarski's Undefinability Theorems, Alonzo Church's Lambda Calculus and its equivalence with Turing machines. Finally, He will discuss the concept of equivalence between programs and proofs as described by the beautiful Curry-Howard Isomorphism Theorem, and how from there emerges the whole concept of computer-assisted formal proofs, studied in Dependent Type Theory.

Speaker: Pedro Abreu

A Bachelor of Computer Science by the University of Brasilia. Master by the University of Purdue (Indiana - USA), host of the podcast Type Theory Forall (https://www.typetheoryforall.com/). He has also been an intern and consultant in different companies working on tests and formal verification, in particular: Tribunal de Contas da União (Federal Court of Accounts, in Brasilia), SiFive (Silicon Valley), Galois (Portland, USA), Nomadic Labs (Paris), Pruvendo (Armenia), etc.