Bra podd
Topplistor
Poddtoppen
Barn och familj
Fritid
Hälsa och motion
Historia
Komedi
Konst och kultur
Musik
Näringsliv
Nyheter och politik
Religion och spiritualitet
Samhälle och kultur
Skönlitteratur
Sport och fritid
Stat och kommun
Teknik
Tv och film
Utbildning
Verkliga brott
Vetenskap
Kategorier
Konst
(1379)
Religion och spiritualitet
(1346)
Utbildning
(1272)
Samhälle och kultur
(1223)
Fritid
(1011)
Teknologi
(991)
Musik
(977)
Vetenskap
(899)
TV och film
(879)
Historia
(823)
Nyheter
(827)
Hälsa och motion
(709)
Näringsliv
(708)
Barn och familj
(677)
Skönlitteratur
(652)
Komedi
(470)
Kristendom
(485)
Böcker
(447)
Verkliga brott
(401)
Sport
(411)
Stat och kommun
(370)
Andlighet
(379)
Självhjälp
(363)
Sällskapsspel
(261)
Drama
(254)
Mental hälsa
(253)
Hobbies
(251)
Musikintervjuer
(234)
Musikkommentarer
(231)
Föräldraskap
(213)
Spel
(217)
Politik
(205)
Dokumentär
(201)
Språkkurs
(192)
Samhällsvetenskap
(172)
Science fiction
(175)
Mat
(142)
Tekniknyheter
(146)
Entreprenörskap
(144)
Filmrecensioner
(143)
Islam
(141)
Dans och teater
(138)
Så gör man
(136)
Investering
(130)
TV-recensioner
(126)
Mode och skönhet
(124)
Personliga dagböcker
(124)
Efterprogram
(120)
Relationer
(120)
Musikhistoria
(124)
Visuell konst
(121)
Berättelser för barn
(112)
Design
(106)
Naturvetenskap
(105)
Nyhetskommentarer
(99)
Filmhistoria
(91)
Karriär
(86)
Kurser
(90)
Life Science
(90)
Hus och trädgård
(89)
Natur
(87)
Filosofi
(86)
Djur
(74)
Medicin
(81)
Fordon
(80)
Alternativ hälsa
(79)
Fotboll
(79)
Ledarskap
(75)
Komedifiktion
(74)
Utbildning för barn
(68)
Underhållningsnyheter
(65)
Religion
(67)
Filmintervjuer
(61)
Dagliga nyheter
(57)
Komediintervjuer
(55)
Affärsnyheter
(52)
Motion
(49)
Marknadsföring
(42)
Hantverk
(46)
Näringslära
(44)
Sexualitet
(35)
Hockey
(38)
Sportnyheter
(38)
Buddhism
(36)
Judendom
(36)
Fysik
(33)
Geovetenskap
(31)
Ideell
(29)
Platser och resor
(28)
Astronomi
(26)
Amerikansk fotboll
(25)
Löpning
(23)
Vildmarken
(22)
Animering och manga
(21)
Flyg
(20)
Improvisering
(20)
Golf
(10)
Matematik
(14)
Hinduism
(13)
Kemi
(11)
Baseball
(3)
Basket
(7)
Tennis
(7)
Ståupp
(6)
Fantasysporter
(3)
Brottning
(2)
Cricket
(2)
Rugby
Simning
Start
/
Iowa Type Theory Commute
/
Point free programming and category theory
Iowa Type Theory Commute
Point-free programming and category theory
7 min • 17 december 2019
Spela avsnitt
Relation of point-free functional programming to category theory.
Spela avsnitt
Senaste avsnitt
Play
Pause
Correction: the Correct Author of the Proof from Last Episode, and an AI flop
12 maj | 7 min
Play
Pause
Krivine's Proof of FD, Using Intersection Types
5 maj | 22 min
Play
Pause
A Measure-Based Proof of Finite Developments
16 april | 23 min
Play
Pause
Introduction to the Finite Developments Theorem
27 mars | 16 min
Play
Pause
Nominal Isabelle/HOL
31 januari | 16 min
Play
Pause
The Locally Nameless Representation
3 januari | 20 min
Play
Pause
POPLmark Reloaded, Part 1
23 december 2024 | 15 min
Play
Pause
POPLmark Reloaded, Part 2
23 december 2024 | 14 min
Play
Pause
Introduction to Formalizing Programming Languages Theory
25 november 2024 | 12 min
Play
Pause
Turing's proof of normalization for STLC
21 maj 2024 | 18 min
Play
Pause
Introduction to normalization for STLC
14 maj 2024 | 10 min
Play
Pause
Arithmetic operations in simply typed lambda calculus
4 maj 2024 | 10 min
Play
Pause
The curious case of exponentiation in simply typed lambda calculus
4 maj 2024 | 7 min
Play
Pause
More on basics of simple types
29 april 2024 | 16 min
Play
Pause
Begin Chapter on Simple Type Theory
19 april 2024 | 16 min
Play
Pause
Some advanced examples in DCS
25 september 2023 | 23 min
Play
Pause
DCS compared to termination checkers for type theories
19 september 2023 | 20 min
Play
Pause
Getting started with DCS
10 september 2023 | 17 min
Play
Pause
Introduction to DCS
4 september 2023 | 12 min
Play
Pause
Semantics of subtyping
24 juli 2023 | 15 min
Play
Pause
More on type inference for simple subtypes
16 juli 2023 | 9 min
Play
Pause
Subtyping, the golden key
9 juli 2023 | 9 min
Play
Pause
Type inference with simple subtypes
30 juni 2023 | 13 min
Play
Pause
Basics of subtyping
21 juni 2023 | 8 min
Play
Pause
Begin chapter on subtyping
21 juni 2023 | 16 min
Play
Pause
Last episode discussing Observational Equality Now for Good
13 april 2023 | 12 min
Play
Pause
More on observational type theory
23 mars 2023 | 14 min
Play
Pause
Introduction to Observational Type Theory
6 mars 2023 | 10 min
Play
Pause
Interjection: The Liquid Tensor Experiment
2 mars 2023 | 12 min
Play
Pause
Extensional Martin-Loef Type Theory
4 februari 2023 | 11 min
Play
Pause
Begin chapter on extensionality
25 januari 2023 | 10 min
Play
Pause
Papers from Formal Methods for Blockchains 2021
1 januari 2023 | 17 min
Play
Pause
Mi-Cho-Coq: Michelson formalized and applied, in Coq
2 december 2022 | 16 min
Play
Pause
Verification of Tezos smart contracts with K-Michelson
11 november 2022 | 14 min
Play
Pause
Start of Season 4: Formal Methods for Blockchain
7 november 2022 | 11 min
Play
Pause
Separation Logic II: recursive predicates
16 september 2022 | 12 min
Play
Pause
Separation Logic 1
25 juli 2022 | 13 min
Play
Pause
Let's talk about Rust
10 juli 2022 | 14 min
Play
Pause
Region-Based Memory Management
22 juni 2022 | 17 min
Play
Pause
Introduction to verified memory management
5 juni 2022 | 17 min
Play
Pause
More on Metamath
21 maj 2022 | 17 min
Play
Pause
Metamath
23 april 2022 | 15 min
Play
Pause
The Seventeen Provers of the World
10 april 2022 | 11 min
Play
Pause
More on Lean
13 mars 2022 | 15 min
Play
Pause
The Lean Prover
28 februari 2022 | 15 min
Play
Pause
More on Isabelle, and the Complexity of ITPs
17 februari 2022 | 16 min
Play
Pause
Isabelle/HOL
28 januari 2022 | 17 min
Play
Pause
More on Agda
13 januari 2022 | 13 min
Play
Pause
A look at Agda
10 januari 2022 | 15 min
Play
Pause
More reflections on Coq
31 december 2021 | 18 min
Play
Pause
The Coq Proof Assistant
29 december 2021 | 15 min
Play
Pause
Introduction to Interactive Theorem Provers
17 december 2021 | 12 min
Play
Pause
The proof-theoretic ordinal of Peano Arithmetic is Epsilon-0
11 december 2021 | 14 min
Play
Pause
The proof-theoretic ordinal of a logical theory
21 november 2021 | 12 min
Play
Pause
Introduction to Ordinal Analysis
17 november 2021 | 15 min
Play
Pause
An analogy for multiplicative disjunction
3 november 2021 | 11 min
Play
Pause
Linear conjunctions and disjunctions
29 oktober 2021 | 12 min
Play
Pause
A taste of linear logic
22 oktober 2021 | 12 min
Play
Pause
Structural rules, or the Curse of the Bound Variable
13 oktober 2021 | 13 min
Play
Pause
Why Cut Elimination is More Complicated than Normalization
5 oktober 2021 | 12 min
Play
Pause
Introduction to Cut Elimination
29 september 2021 | 9 min
Play
Pause
Normalization of detours for implication inferences
19 september 2021 | 13 min
Play
Pause
Normalization in natural deduction
18 september 2021 | 11 min
Play
Pause
A Brief Look at Sequent Calculus
16 september 2021 | 12 min
Play
Pause
Natural deduction: or, the bad news!
14 september 2021 | 12 min
Play
Pause
Implication rules for natural deduction
14 september 2021 | 12 min
Play
Pause
Natural Deduction
12 september 2021 | 12 min
Play
Pause
Rules of proof, standard proof systems
9 september 2021 | 13 min
Play
Pause
Different proof systems, distinguishing logical rules from domain axioms
2 september 2021 | 12 min
Play
Pause
Introduction to Proof Theory (Start of Season 3)
31 augusti 2021 | 18 min
Play
Pause
Modula-2
28 juli 2021 | 11 min
Play
Pause
Decomposing recursions using algebras
13 juli 2021 | 12 min
Play
Pause
Reassembling datatypes from functors using a fixed-point
11 juli 2021 | 10 min
Play
Pause
Decomposing datatypes into functors
3 juli 2021 | 14 min
Play
Pause
Modular datatypes: introducing Swierstra's paper "Datatypes à la Carte"
24 juni 2021 | 9 min
Play
Pause
Modules for Mathematical Theories (MMT)
9 juni 2021 | 12 min
Play
Pause
Some thoughts on module systems so far
19 maj 2021 | 12 min
Play
Pause
A look at Agda's module system
12 maj 2021 | 14 min
Play
Pause
Standard ML: the Newmar King-Aire of module systems
10 maj 2021 | 14 min
Play
Pause
A look at Haskell's module system
27 april 2021 | 22 min
Play
Pause
Let's talk about modules!
20 april 2021 | 21 min
Play
Pause
Church-style Typing and Intersection Types: Glimpses of Benjamin Pierce's Dissertation
12 april 2021 | 13 min
Play
Pause
Intersections and Unions in Practice; Failure of Type Preservation with Unions
22 mars 2021 | 14 min
Play
Pause
Normal terms are typable with intersection types
5 mars 2021 | 10 min
Play
Pause
Intersection Types Preserved Under Beta-Expansion
15 februari 2021 | 12 min
Play
Pause
Introduction to Intersection Types
9 februari 2021 | 12 min
Play
Pause
Deriving disjointness of constructor ranges in RelTT
2 februari 2021 | 12 min
Play
Pause
Software Design and Intrinsic Identity
21 januari 2021 | 9 min
Play
Pause
Identity Inclusion in Relational Type Theory
18 januari 2021 | 14 min
Play
Pause
On the paper "The Girard-Reynolds Isomorphism" by Philip Wadler
18 januari 2021 | 11 min
Play
Pause
Equivalence of inductive and parametric naturals in RelTT
28 december 2020 | 14 min
Play
Pause
Examples in Relational Type Theory
23 december 2020 | 23 min
Play
Pause
The Semantics of Relational Types
23 december 2020 | 21 min
Play
Pause
Introducing Relational Type Theory
15 december 2020 | 13 min
Play
Pause
The Types of Relational Type Theory
15 december 2020 | 15 min
Play
Pause
On the paper "Types, Abstraction, and Parametric Polymorphism"
26 november 2020 | 21 min
Play
Pause
Explaining my encoding of a HOAS datatype, part 2
9 november 2020 | 19 min
Play
Pause
Parametric models and representation independence
9 november 2020 | 19 min
Play
Pause
Explaining my encoding of a HOAS datatype, part 1
19 oktober 2020 | 10 min
Play
Pause
Term models for higher-order signatures
19 oktober 2020 | 14 min
Play
Pause
Lambda applicative structures and interpretations of lambda abstractions
8 oktober 2020 | 10 min
Play
Pause
The Basic Lemma
30 september 2020 | 15 min
Play
Pause
Logical relations are not closed under composition
31 augusti 2020 | 10 min
Play
Pause
The definition of a logical relation
19 augusti 2020 | 11 min
Play
Pause
Introduction to Logical Relations
17 augusti 2020 | 12 min
Play
Pause
Lamping's abstract algorithm
25 juli 2020 | 10 min
Play
Pause
Examples showing non-optimality of Haskell
15 juli 2020 | 20 min
Play
Pause
Lambda graphs with duplicators and start of Lamping's abstract algorithm
3 juli 2020 | 22 min
Play
Pause
Duplicating redexes as the central problem of optimal reduction
21 juni 2020 | 16 min
Play
Pause
Introduction to optimal beta reduction
16 juni 2020 | 17 min
Play
Pause
Lexicographic termination
3 juni 2020 | 11 min
Play
Pause
Well-founded recursion
19 maj 2020 | 15 min
Play
Pause
Mendler-style iteration
19 maj 2020 | 11 min
Play
Pause
Compositional termination checking with sized types
30 mars 2020 | 19 min
Play
Pause
Noncompositionality of syntactic structural-recursion checks
20 mars 2020 | 13 min
Play
Pause
Structural termination
17 mars 2020 | 16 min
Play
Pause
Proving Confluence for Untyped Lambda Calculus II
13 mars 2020 | 12 min
Play
Pause
Proving Confluence for Untyped Lambda Calculus I
13 mars 2020 | 12 min
Play
Pause
Confluence, and its use for conversion checking
11 mars 2020 | 15 min
Play
Pause
Normalization and logical consistency
9 mars 2020 | 15 min
Play
Pause
Normalization in type theory: where it is needed, and where not
6 mars 2020 | 16 min
Play
Pause
Introduction to normalization
6 mars 2020 | 13 min
Play
Pause
Proving type safety; upcoming metatheoretic properties
4 mars 2020 | 13 min
Play
Pause
The progress property and the problem of axioms in type theory
4 mars 2020 | 10 min
Play
Pause
Introduction to type safety
2 mars 2020 | 14 min
Play
Pause
Introduction to metatheory
28 februari 2020 | 12 min
Play
Pause
Definition of the Mendler encoding
26 februari 2020 | 16 min
Play
Pause
The Mendler encoding and the problem of explicit recursion
25 februari 2020 | 11 min
Play
Pause
The Scott encoding
24 februari 2020 | 16 min
Play
Pause
More on the Parigot encoding
22 februari 2020 | 12 min
Play
Pause
Introduction to the Parigot encoding
18 februari 2020 | 12 min
Play
Pause
Church-encoding natural numbers
17 februari 2020 | 12 min
Play
Pause
Church encoding of lists
15 februari 2020 | 11 min
Play
Pause
Church encoding of the booleans
15 februari 2020 | 11 min
Play
Pause
Introduction to Church encoding
12 februari 2020 | 10 min
Play
Pause
Functional encodings turning the world inside out
11 februari 2020 | 9 min
Play
Pause
More benefits of lambda encodings
7 februari 2020 | 12 min
Play
Pause
Introduction to lambda encodings
7 februari 2020 | 14 min
Play
Pause
Adding a top type and allowing non-normalizing terms
5 februari 2020 | 14 min
Play
Pause
Intersection types using Curry-style typing
4 februari 2020 | 11 min
Play
Pause
Curry-style versus Church-style, and the nature of type annotations
30 januari 2020 | 13 min
Play
Pause
More on Computation First, and Basic Idea of Realizability
29 januari 2020 | 16 min
Play
Pause
Types should be erased for executing and reasoning about programs
29 januari 2020 | 13 min
Play
Pause
Why go beyond GADTs?
24 januari 2020 | 12 min
Play
Pause
GADTs for programming with representations of types
22 januari 2020 | 16 min
Play
Pause
Using GADTs for typed subsetting of your language
20 januari 2020 | 15 min
Play
Pause
Example of programming with indexed types: binary search trees
16 januari 2020 | 11 min
Play
Pause
Programming with indexed types using singletons
16 januari 2020 | 12 min
Play
Pause
Limitations of indexed types that are not truly dependent
14 januari 2020 | 14 min
Play
Pause
Programming with Indexed Types
13 januari 2020 | 12 min
Play
Pause
Program Termination and the Curry-Howard Isomorphism
10 januari 2020 | 11 min
Play
Pause
Why Curry-Howard for classical proofs is a bad idea for programming
7 januari 2020 | 14 min
Play
Pause
Curry-Howard for classical logic
6 januari 2020 | 12 min
Play
Pause
Dependent types and design by contract
4 januari 2020 | 10 min
Play
Pause
Indexed types and Curry-Howard for first-order quantifiers
3 januari 2020 | 9 min
Play
Pause
The Curry-Howard Isomorphism for Propositional Logic
2 januari 2020 | 13 min
Play
Pause
The Curry-Howard Isomorphism for Induction
31 december 2019 | 12 min
Play
Pause
Constructive proofs as programs
22 december 2019 | 10 min
Play
Pause
Functors and catamorphisms
20 december 2019 | 13 min
Play
Pause
Introduction to the Curry-Howard Isomorphism
20 december 2019 | 16 min
Play
Pause
Structured Recursion Schemes for Point-Free Recursion
19 december 2019 | 13 min
Play
Pause
More on point-free programming and category theory
17 december 2019 | 13 min
Play
Pause
Point-free programming and category theory
17 december 2019 | 7 min
Play
Pause
Concise code through point-free programming
13 december 2019 | 7 min
Play
Pause
More on FP and concise code
12 december 2019 | 10 min
Play
Pause
Functional Programming and Concise Code: Type Inference
12 december 2019 | 9 min
Play
Pause
Introduction to Functional Programming
11 december 2019 | 8 min
Play
Pause
Software Engineering Considerations for Formal Methods
2 december 2019 | 16 min
Play
Pause
Power of Computer-Checked Proofs for Software
1 december 2019 | 12 min
Play
Pause
Technical reasons for lack of adoption of computer-checked proofs
28 november 2019 | 10 min
Play
Pause
Why Computer-Checked Proofs are Not Used More in Mathematics
27 november 2019 | 10 min
Play
Pause
Computer-Checked Proofs in American Research
26 november 2019 | 14 min
Play
Pause
Computer-checked proofs about software
24 november 2019 | 8 min
Play
Pause
More on Computer-Checked Proofs
22 november 2019 | 14 min
Play
Pause
Computer-checked proofs
21 november 2019 | 14 min
Ladda fler
Minimera
00:00
-00:00
15
Tillbaka 15 sekunder
Play
Pause
15
Framåt 15 sekunder
15
Tillbaka 15 sekunder
Play
Pause
15
Framåt 15 sekunder
Expandera spelare
Stäng spelare
00:00
-00:00