Menu
My Activity Hub
Podcasts
Videos
Pricing
Feedback
Tutoring
Sign Up
Log In
My Activity Hub
Podcasts
Videos
How it works
Pricing
Tutoring
Sign Up
Log In
Iowa Type Theory Commute
Aaron Stump talks about type theory, computational logic, and related topics in Computer Science on his short commute.
The Semantics of Relational Types
21 mins; December 22, 2020
Introducing Relational Type Theory
13 mins; December 14, 2020
The Types of Relational Type Theory
14 mins; December 14, 2020
On the paper "Types, Abstraction, and Parametric Polymorphism"
21 mins; November 25, 2020
Explaining my encoding of a HOAS datatype, part 2
18 mins; November 09, 2020
Parametric models and representation independence
18 mins; November 09, 2020
Explaining my encoding of a HOAS datatype, part 1
10 mins; October 19, 2020
Term models for higher-order signatures
14 mins; October 19, 2020
Lambda applicative structures and interpretations of lambda abstractions
10 mins; October 07, 2020
The Basic Lemma
14 mins; September 30, 2020
Logical relations are not closed under composition
10 mins; August 31, 2020
The definition of a logical relation
10 mins; August 18, 2020
Introduction to Logical Relations
12 mins; August 16, 2020
Lamping's abstract algorithm
10 mins; July 25, 2020
Examples showing non-optimality of Haskell
19 mins; July 14, 2020
Lambda graphs with duplicators and start of Lamping's abstract algorithm
22 mins; July 03, 2020
Duplicating redexes as the central problem of optimal reduction
16 mins; June 20, 2020
Introduction to optimal beta reduction
16 mins; June 16, 2020
Lexicographic termination
11 mins; June 02, 2020
Well-founded recursion
15 mins; May 18, 2020
Mendler-style iteration
10 mins; May 18, 2020
Compositional termination checking with sized types
18 mins; March 30, 2020
Noncompositionality of syntactic structural-recursion checks
13 mins; March 19, 2020
Structural termination
16 mins; March 17, 2020
Proving Confluence for Untyped Lambda Calculus II
12 mins; March 13, 2020
Proving Confluence for Untyped Lambda Calculus I
11 mins; March 13, 2020
Confluence, and its use for conversion checking
15 mins; March 11, 2020
Normalization and logical consistency
14 mins; March 09, 2020
Normalization in type theory: where it is needed, and where not
16 mins; March 06, 2020
Introduction to normalization
12 mins; March 05, 2020
Proving type safety; upcoming metatheoretic properties
13 mins; March 04, 2020
The progress property and the problem of axioms in type theory
10 mins; March 03, 2020
Introduction to type safety
14 mins; March 02, 2020
Introduction to metatheory
11 mins; February 28, 2020
Definition of the Mendler encoding
15 mins; February 26, 2020
The Mendler encoding and the problem of explicit recursion
10 mins; February 25, 2020
The Scott encoding
16 mins; February 24, 2020
More on the Parigot encoding
11 mins; February 21, 2020
Introduction to the Parigot encoding
11 mins; February 18, 2020
Church-encoding natural numbers
11 mins; February 17, 2020
Church encoding of lists
10 mins; February 14, 2020
Church encoding of the booleans
11 mins; February 14, 2020
Introduction to Church encoding
10 mins; February 11, 2020
Functional encodings turning the world inside out
8 mins; February 11, 2020
More benefits of lambda encodings
11 mins; February 07, 2020
Introduction to lambda encodings
13 mins; February 07, 2020
Adding a top type and allowing non-normalizing terms
14 mins; February 04, 2020
Intersection types using Curry-style typing
10 mins; February 04, 2020
Curry-style versus Church-style, and the nature of type annotations
13 mins; January 30, 2020
More on Computation First, and Basic Idea of Realizability
15 mins; January 29, 2020
Types should be erased for executing and reasoning about programs
12 mins; January 29, 2020
Why go beyond GADTs?
12 mins; January 24, 2020
GADTs for programming with representations of types
15 mins; January 22, 2020
Using GADTs for typed subsetting of your language
14 mins; January 20, 2020
Example of programming with indexed types: binary search trees
10 mins; January 16, 2020
Programming with indexed types using singletons
11 mins; January 16, 2020
Limitations of indexed types that are not truly dependent
14 mins; January 14, 2020
Programming with Indexed Types
12 mins; January 13, 2020
Program Termination and the Curry-Howard Isomorphism
10 mins; January 10, 2020
Why Curry-Howard for classical proofs is a bad idea for programming
14 mins; January 06, 2020
Curry-Howard for classical logic
11 mins; January 06, 2020
Dependent types and design by contract
9 mins; January 03, 2020
Indexed types and Curry-Howard for first-order quantifiers
9 mins; January 03, 2020
The Curry-Howard Isomorphism for Propositional Logic
13 mins; January 02, 2020
The Curry-Howard Isomorphism for Induction
11 mins; December 31, 2019
Constructive proofs as programs
9 mins; December 21, 2019
Functors and catamorphisms
12 mins; December 20, 2019
Introduction to the Curry-Howard Isomorphism
15 mins; December 20, 2019
Structured Recursion Schemes for Point-Free Recursion
12 mins; December 18, 2019
More on point-free programming and category theory
13 mins; December 17, 2019
Point-free programming and category theory
6 mins; December 17, 2019
Concise code through point-free programming
6 mins; December 13, 2019
More on FP and concise code
9 mins; December 12, 2019
Functional Programming and Concise Code: Type Inference
9 mins; December 12, 2019
Introduction to Functional Programming
7 mins; December 11, 2019
Software Engineering Considerations for Formal Methods
16 mins; December 01, 2019
Power of Computer-Checked Proofs for Software
11 mins; November 30, 2019
Technical reasons for lack of adoption of computer-checked proofs
10 mins; November 28, 2019
Why Computer-Checked Proofs are Not Used More in Mathematics
9 mins; November 27, 2019
Computer-Checked Proofs in American Research
13 mins; November 26, 2019
Computer-checked proofs about software
8 mins; November 23, 2019
More on Computer-Checked Proofs
13 mins; November 22, 2019
Computer-checked proofs
14 mins; November 21, 2019
Click here to see more
‹ Prev
1
2
Next ›
