Skip to content
Hallway
0:00 / 0:00

#lambdacalculus#turingmachine#philipwadler

Philip Wadler: Church's Coincidences

princetonacademics

9.4K subscribers • 3 videos on Hallway

YouTube
  • Recommended by 2 people: 1 in engineering communities and 1 curated list.
  • Presented by Philip Wadler, Professor of Theoretical Computer Science at the University of Edinburgh

Intermediate. Assumes working knowledge.

11K views14 years ago2 recommendations

Computer scienceHistory and cultureComputation and complexityHistory of computingPeople who shaped computing

Philip Wadler explores the foundational equivalence between Church's lambda calculus, Gödel's recursive functions, and Turing machines.

Philip Wadler, Professor of Theoretical Computer Science at the University of Edinburgh, contends that the foundations of computing lay in a coincidence: Church's lambda calculus (1933), Herbrand and Godel's recursive functions (1934), and Turing's machines (1935) all defined the same model of computation. He gave this lecture on the occasion of Princeton University's centennial celebration of Alan Turing. Learn more at www.princeton.edu/turing #turingprinceton

Why it's here

2 people recommend this

What people say. Recommended as an engaging and historic lecture on the deep mathematical connections at the foundation of computer science.

Moments people linked to

u/Condexin r/compsci • Recommends

Philip Wadler: Church's Coincidences
11View on Reddit

programming-talkscurated list on GitHubRecommends

Under “Theoretical Computer Science”

Church's Coincidences 01:03:41 by **Philip Wadler** (2012)
View the list

u/Condexin r/ProgrammingLanguages • Mentions

On “Do i need to be an expert in type theory to make a PL?”

The Short Answer: No. The Long Answer: I really like static typing and type theory. I think it's the right thing to do. However, I also appreciate that understanding types is a non-trivial exercise. There are different types of type theory and there's different implementations of the same type theories. Take Agda vs Idris for example. They're both dependently typed languages, but Idris uses heterogeneous propositional equality and Agda uses homogeneous propositional equality. I actually don't really understand all of what that means, but apparently it has non-trivial implications as to what you can implement using these languages (Homotopy Type Theory is supposedly incompatible with…
14View on Reddit

u/Condexin r/compsci • Mentions

On “Category Theory for the Working Hacker”

This talk is by Philip Wadler. He has got to be my favorite speaker for computational theory topics. Very enjoyable for a topic which is easy to be very dry. My favorite Wadler talk has got to be: link to this video
3View on Reddit

u/PM_ME_UR_OBSIDIANin r/compsci • Mentions

On “Philip Wadler: Church's Coincidences”

That introduction was unbearable. The presentation proper starts at 4:40. In any case, this is pretty much the same talk as *Propositions as Types*, which has a better recording.
1View on Reddit