Iowa Type Theory Commute

View Top 200 Chart

Back to Rankings Page

Technology
**Iowa Type Theory Commute**

Aaron Stump talks about type theory, computational logic, and related topics in Computer Science on his short commute.

Latest Episodes:

Introduction to Church encoding Feb 11, 2020

Show notes

The Church encoding represents data as their own fold-right functions

Functional encodings turning the world inside out Feb 11, 2020

Show notes

Functional encodings take programming language features like pattern-matching and recursion and move them from outside of data to inside of data.

More benefits of lambda encodings Feb 07, 2020

Show notes

The idea that without lambda encodings, the current state of the art forces you to commit to a class of datatypes in the design of your type theory.

Introduction to lambda encodings Feb 07, 2020

Show notes

A lambda encoding is some way of representing data as functions (lambda abstractions). Some motivations for this for computer-checked proofs and type theory.

Adding a top type and allowing non-normalizing terms Feb 04, 2020

Show notes

Curry-style typing and realizability make it sensible to allow a top type to type every term, even non-normalizing ones.

Intersection types using Curry-style typing Feb 04, 2020

Show notes

Intersection types internalize the idea that a term has two types. Curry-style typing is generally needed for this to be nontrivial.

Curry-style versus Church-style, and the nature of type annotations Jan 30, 2020

Show notes

In Curry-style typing annotations -- for example, the types of bound variables -- are erased, and not truly (semantically) part of the term. In Church-style, they are intrinsic to the term and are truly there. Discussion of some of the practicalities of Curry-style typing, in particular type annotations versus proving typings.

More on Computation First, and Basic Idea of Realizability Jan 29, 2020

Show notes

Types are specifications whose semantics is explained in terms of computation, which is thus conceptually prior. Realizability is a way of explaining the semantics of types.

Types should be erased for executing and reasoning about programs Jan 29, 2020

Show notes

In which I argue that type information should be erased from programs by the compiler both for final execution and also for reasoning (in a language with dependent types, for example, where we can reason about program execution statically).

Why go beyond GADTs? Jan 24, 2020

Show notes

GADTs are quite powerful. Why go all the way to true dependent types? And should you use the Curry-Howard isomorphism (see Chapter 3 of the podcast) or not?

Our TOPPODCAST Picks

Follow Us

Stay Connected

Related Podcasts

Links

Stay Connected

Our TOPPODCAST Picks

Follow Us

Stay Connected

Iowa Type Theory Commute

Related Podcasts

1

2

3

4

5

6