Канал: Type Theory Forall

#39 Equality, Quotation, Bidirectional Type Checking - David Christiansen

#39 Equality, Quotation, Bidirectional Type Checking - David Christiansen

#38 Haskell, Lean, Idris, and the Art of Writing - David Christiansen

#38 Haskell, Lean, Idris, and the Art of Writing - David Christiansen

#37 Compilers, Staging, Futamura Projections - Guannan Wei

#37 Compilers, Staging, Futamura Projections - Guannan Wei

#36 Behind the Person Behind this Podcast - Pedro Abreu

#36 Behind the Person Behind this Podcast - Pedro Abreu

#35 Teika, Self-Education and F***ing Floating Points - Eduardo Rafael

#35 Teika, Self-Education and F***ing Floating Points - Eduardo Rafael

#34 Foundations of Theorem Provers and Cedille2 - Andrew Marmaduke

#34 Foundations of Theorem Provers and Cedille2 - Andrew Marmaduke

#33 Z3 and Lean, the Spiritual Journey - Leo de Moura

#33 Z3 and Lean, the Spiritual Journey - Leo de Moura

#32 TyDe Systems - Jan de Muijnck-Hughes

#32 TyDe Systems - Jan de Muijnck-Hughes

#31 Discussing Problems in PL and Academia - Jan de Muijnck-Hughes

#31 Discussing Problems in PL and Academia - Jan de Muijnck-Hughes

#30 Actors, GADTs and Burnout - Dan and Pedro

#30 Actors, GADTs and Burnout - Dan and Pedro

#29 Can PL theory make you a better software engineer? - Jimmy Koppel

#29 Can PL theory make you a better software engineer? - Jimmy Koppel

#28 Formally Verifying Smart Contracts - Pruvendo

#28 Formally Verifying Smart Contracts - Pruvendo

#27 Formalizing an OS: The seL4 - Gerwin Klein

#27 Formalizing an OS: The seL4 - Gerwin Klein

#26 Mechanizing Modern Mathematics - Kevin Buzzard

#26 Mechanizing Modern Mathematics - Kevin Buzzard

#25 Formally Verifying the Tezos Codebase - Formal Land

#25 Formally Verifying the Tezos Codebase - Formal Land

#24 The History of Isabelle - Lawrence Paulson

#24 The History of Isabelle - Lawrence Paulson

#23 What is the SIGPLAN? - Jens Palsberg and Jonathan Aldrich

#23 What is the SIGPLAN? - Jens Palsberg and Jonathan Aldrich

#22 Impredicativity, LEM, Realizability and more - Cody Roux

#22 Impredicativity, LEM, Realizability and more - Cody Roux

#21 Denotational Design - Conal Elliott

#21 Denotational Design - Conal Elliott

#20 Huaweii, String Diagrams, Game Semantics - Dan R. Ghica

#20 Huaweii, String Diagrams, Game Semantics - Dan R. Ghica

#19 Experience Report: Learning Coq - Patrick and Supun

#19 Experience Report: Learning Coq - Patrick and Supun

#18 Gödel's Incompleteness Theorems - Cody Roux

#18 Gödel's Incompleteness Theorems - Cody Roux

#17 The Lost Elegance of Computation - Conal Elliott

#17 The Lost Elegance of Computation - Conal Elliott

#16 Agda, K Axiom, HoTT, Rewrite Theory - Jesper Cockx

#16 Agda, K Axiom, HoTT, Rewrite Theory - Jesper Cockx

#15 Coq Projects, Agda, Idris, Kind - Nitin and Eric

#15 Coq Projects, Agda, Idris, Kind - Nitin and Eric

#14 POPL, Parametricity, Scala, DOT - Nitin and Eric

#14 POPL, Parametricity, Scala, DOT - Nitin and Eric

#13 C/C++, Emacs, Haskell, and Coq. The Journey - John Wiegley

#13 C/C++, Emacs, Haskell, and Coq. The Journey - John Wiegley

#12 Tenure, Sexism and ADHD - Talia Ringer

#12 Tenure, Sexism and ADHD - Talia Ringer

#11 FP, Monads, GHC, and beyond - Alejandro Serrano

#11 FP, Monads, GHC, and beyond - Alejandro Serrano

#10 Classical Logic vs Intuitionistic Logic - Thorsten Altenkirch and Anupam Das

#10 Classical Logic vs Intuitionistic Logic - Thorsten Altenkirch and Anupam Das

#9 Logic and Proof Theory - Anupam Das

#9 Logic and Proof Theory - Anupam Das

#8 Cedille - Chris Jenkins

#8 Cedille - Chris Jenkins

#7 Hacking Isabelle's Internals - Hacking Isabelle's Internals

#7 Hacking Isabelle's Internals - Hacking Isabelle's Internals

#6 All The Dumb Questions on Gradual Types - Zeina Migeed

#6 All The Dumb Questions on Gradual Types - Zeina Migeed

#5 The History of Coq'Art - Yves Bertot

#5 The History of Coq'Art - Yves Bertot

#4 Theorem Provers, Functional Programming and Companies - Eric Bond

#4 Theorem Provers, Functional Programming and Companies - Eric Bond

#3 ML for PL and Mental Health - Dan Zheng

#3 ML for PL and Mental Health - Dan Zheng

#2 Grad School Life - Rajan Walia and John Sarracino

#2 Grad School Life - Rajan Walia and John Sarracino

#1 What is PL research? - Prof. Ben Delaware

#1 What is PL research? - Prof. Ben Delaware

#0 Cool Internships in PL - Pedro Abreu

#0 Cool Internships in PL - Pedro Abreu