YoVDO

Propositions as Types

Offered By: Strange Loop Conference via YouTube

Tags

Strange Loop Conference Courses Programming Languages Courses Logic Courses Functional Programming Courses Lambda Calculus Courses Type Theory Courses

Course Description

Overview

Explore the profound connection between logic and computation in this 43-minute conference talk from Strange Loop. Delve into the principle of Propositions as Types, uncovering its far-reaching impact on theorem provers and programming language design. Discover the depth, breadth, and mystery behind this concept, which goes by many names and has multiple origins. Examine why functional programming both is and isn't the universal programming language. Join Professor Philip Wadler, a distinguished computer scientist from the University of Edinburgh, as he guides you through topics including David Hilbert's work, incompleteness theorems, lambda calculus, Turing machines, natural deduction, type theory, and the philosophical implications of multiverses. Gain insights from Wadler's extensive experience in academia and industry, and his contributions to languages like Haskell, Java, and XQuery.

Syllabus

Introduction
David Hilbert
Antidual problem
Incompleteness theorem
Alonzo Church
lambda calculus
girdle
Turing machines
Is mathematics invented
Natural Deduction
Formal Proof
Sub Formula Property
Example
Type Theory
Evaluation
Holding problem
Evaluation of programs
History
Polymorphic lambda calculus
Philosophy
Multiverses
Questions


Taught by

Strange Loop Conference

Tags

Related Courses

Functional Programming Principles in Scala
École Polytechnique Fédérale de Lausanne via Coursera
Functional Program Design in Scala
École Polytechnique Fédérale de Lausanne via Coursera
Paradigms of Computer Programming
Université catholique de Louvain via edX
Introduction to Functional Programming
Delft University of Technology via edX
Paradigms of Computer Programming – Fundamentals
Université catholique de Louvain via edX