Iowa Type Theory CommuteIowa Type Theory CommuteWhat is Control Flow Analysis for Lambda Calculus?What is Control Flow Analysis for Lambda Calculus?Measure Functions and Termination of STLCMeasure Functions and Termination of STLCSchematic Affine Recursion, Oh My!Schematic Affine Recursion, Oh My!The Stunner: Linear System T is Diverging!The Stunner: Linear System T is Diverging!Terminating Computation First?Terminating Computation First?Correction: the Correct Author of the Proof from Last Episode, and an AI flopCorrection: the Correct Author of the Proof from Last Episode, and an AI flopKrivine's Proof of FD, Using Intersection TypesKrivine's Proof of FD, Using Intersection TypesA Measure-Based Proof of Finite DevelopmentsA Measure-Based Proof of Finite DevelopmentsIntroduction to the Finite Developments TheoremIntroduction to the Finite Developments TheoremNominal Isabelle/HOLNominal Isabelle/HOLThe Locally Nameless RepresentationThe Locally Nameless RepresentationPOPLmark Reloaded, Part 2POPLmark Reloaded, Part 2POPLmark Reloaded, Part 1POPLmark Reloaded, Part 1Introduction to Formalizing Programming Languages TheoryIntroduction to Formalizing Programming Languages TheoryTuring's proof of normalization for STLCTuring's proof of normalization for STLCIntroduction to normalization for STLCIntroduction to normalization for STLCThe curious case of exponentiation in simply typed lambda calculusThe curious case of exponentiation in simply typed lambda calculusArithmetic operations in simply typed lambda calculusArithmetic operations in simply typed lambda calculusMore on basics of simple typesMore on basics of simple typesBegin Chapter on Simple Type TheoryBegin Chapter on Simple Type TheorySome advanced examples in DCSSome advanced examples in DCSDCS compared to termination checkers for type theoriesDCS compared to termination checkers for type theoriesGetting started with DCSGetting started with DCSIntroduction to DCSIntroduction to DCSSemantics of subtypingSemantics of subtypingMore on type inference for simple subtypesMore on type inference for simple subtypesSubtyping, the golden keySubtyping, the golden keyType inference with simple subtypesType inference with simple subtypesBasics of subtypingBasics of subtypingBegin chapter on subtypingBegin chapter on subtypingLast episode discussing Observational Equality Now for GoodLast episode discussing Observational Equality Now for GoodMore on observational type theoryMore on observational type theoryIntroduction to Observational Type TheoryIntroduction to Observational Type TheoryInterjection: The Liquid Tensor ExperimentInterjection: The Liquid Tensor ExperimentExtensional Martin-Loef Type TheoryExtensional Martin-Loef Type TheoryBegin chapter on extensionalityBegin chapter on extensionalityPapers from Formal Methods for Blockchains 2021Papers from Formal Methods for Blockchains 2021Mi-Cho-Coq: Michelson formalized and applied, in CoqMi-Cho-Coq: Michelson formalized and applied, in CoqVerification of Tezos smart contracts with K-Michelson Verification of Tezos smart contracts with K-Michelson Start of Season 4: Formal Methods for BlockchainStart of Season 4: Formal Methods for BlockchainSeparation Logic II: recursive predicatesSeparation Logic II: recursive predicatesSeparation Logic 1Separation Logic 1Let's talk about RustLet's talk about RustRegion-Based Memory ManagementRegion-Based Memory ManagementIntroduction to verified memory managementIntroduction to verified memory managementMore on MetamathMore on MetamathMetamathMetamathThe Seventeen Provers of the WorldThe Seventeen Provers of the WorldMore on LeanMore on LeanThe Lean ProverThe Lean ProverMore on Isabelle, and the Complexity of ITPsMore on Isabelle, and the Complexity of ITPsIsabelle/HOLIsabelle/HOLMore on AgdaMore on AgdaA look at AgdaA look at AgdaMore reflections on CoqMore reflections on CoqThe Coq Proof AssistantThe Coq Proof AssistantIntroduction to Interactive Theorem ProversIntroduction to Interactive Theorem ProversThe proof-theoretic ordinal of Peano Arithmetic is Epsilon-0The proof-theoretic ordinal of Peano Arithmetic is Epsilon-0The proof-theoretic ordinal of a logical theoryThe proof-theoretic ordinal of a logical theoryIntroduction to Ordinal AnalysisIntroduction to Ordinal AnalysisAn analogy for multiplicative disjunctionAn analogy for multiplicative disjunctionLinear conjunctions and disjunctionsLinear conjunctions and disjunctionsA taste of linear logicA taste of linear logicStructural rules, or the Curse of the Bound VariableStructural rules, or the Curse of the Bound VariableWhy Cut Elimination is More Complicated than NormalizationWhy Cut Elimination is More Complicated than NormalizationIntroduction to Cut EliminationIntroduction to Cut EliminationNormalization of detours for implication inferencesNormalization of detours for implication inferencesNormalization in natural deductionNormalization in natural deductionA Brief Look at Sequent CalculusA Brief Look at Sequent CalculusNatural deduction: or, the bad news!Natural deduction: or, the bad news!Implication rules for natural deductionImplication rules for natural deductionNatural DeductionNatural DeductionRules of proof, standard proof systemsRules of proof, standard proof systemsDifferent proof systems, distinguishing logical rules from domain axiomsDifferent proof systems, distinguishing logical rules from domain axiomsIntroduction to Proof Theory (Start of Season 3)Introduction to Proof Theory (Start of Season 3)Modula-2Modula-2Decomposing recursions using algebrasDecomposing recursions using algebrasReassembling datatypes from functors using a fixed-point Reassembling datatypes from functors using a fixed-point Decomposing datatypes into functorsDecomposing datatypes into functorsModular datatypes: introducing Swierstra's paper "Datatypes à la Carte"Modular datatypes: introducing Swierstra's paper "Datatypes à la Carte"Modules for Mathematical Theories (MMT)Modules for Mathematical Theories (MMT)Some thoughts on module systems so farSome thoughts on module systems so farA look at Agda's module systemA look at Agda's module systemStandard ML: the Newmar King-Aire of module systemsStandard ML: the Newmar King-Aire of module systemsA look at Haskell's module systemA look at Haskell's module systemLet's talk about modules!Let's talk about modules!Church-style Typing and Intersection Types: Glimpses of Benjamin Pierce's DissertationChurch-style Typing and Intersection Types: Glimpses of Benjamin Pierce's DissertationIntersections and Unions in Practice; Failure of Type Preservation with UnionsIntersections and Unions in Practice; Failure of Type Preservation with UnionsNormal terms are typable with intersection typesNormal terms are typable with intersection typesIntersection Types Preserved Under Beta-ExpansionIntersection Types Preserved Under Beta-ExpansionIntroduction to Intersection TypesIntroduction to Intersection TypesDeriving disjointness of constructor ranges in RelTTDeriving disjointness of constructor ranges in RelTTSoftware Design and Intrinsic IdentitySoftware Design and Intrinsic IdentityIdentity Inclusion in Relational Type TheoryIdentity Inclusion in Relational Type TheoryOn the paper "The Girard-Reynolds Isomorphism" by Philip WadlerOn the paper "The Girard-Reynolds Isomorphism" by Philip WadlerEquivalence of inductive and parametric naturals in RelTTEquivalence of inductive and parametric naturals in RelTTExamples in Relational Type TheoryExamples in Relational Type TheoryThe Semantics of Relational TypesThe Semantics of Relational TypesThe Types of Relational Type TheoryThe Types of Relational Type TheoryIntroducing Relational Type TheoryIntroducing Relational Type TheoryOn the paper "Types, Abstraction, and Parametric Polymorphism"On the paper "Types, Abstraction, and Parametric Polymorphism"Parametric models and representation independenceParametric models and representation independenceExplaining my encoding of a HOAS datatype, part 2Explaining my encoding of a HOAS datatype, part 2Explaining my encoding of a HOAS datatype, part 1Explaining my encoding of a HOAS datatype, part 1Term models for higher-order signaturesTerm models for higher-order signaturesLambda applicative structures and interpretations of lambda abstractionsLambda applicative structures and interpretations of lambda abstractionsThe Basic LemmaThe Basic LemmaLogical relations are not closed under compositionLogical relations are not closed under compositionThe definition of a logical relationThe definition of a logical relationIntroduction to Logical RelationsIntroduction to Logical RelationsLamping's abstract algorithmLamping's abstract algorithmExamples showing non-optimality of HaskellExamples showing non-optimality of HaskellLambda graphs with duplicators and start of Lamping's abstract algorithmLambda graphs with duplicators and start of Lamping's abstract algorithmDuplicating redexes as the central problem of optimal reductionDuplicating redexes as the central problem of optimal reductionIntroduction to optimal beta reductionIntroduction to optimal beta reductionLexicographic terminationLexicographic terminationMendler-style iterationMendler-style iterationWell-founded recursionWell-founded recursionCompositional termination checking with sized typesCompositional termination checking with sized typesNoncompositionality of syntactic structural-recursion checksNoncompositionality of syntactic structural-recursion checksStructural terminationStructural terminationProving Confluence for Untyped Lambda Calculus IIProving Confluence for Untyped Lambda Calculus IIProving Confluence for Untyped Lambda Calculus IProving Confluence for Untyped Lambda Calculus IConfluence, and its use for conversion checkingConfluence, and its use for conversion checkingNormalization and logical consistencyNormalization and logical consistencyNormalization in type theory: where it is needed, and where notNormalization in type theory: where it is needed, and where notIntroduction to normalizationIntroduction to normalizationProving type safety; upcoming metatheoretic propertiesProving type safety; upcoming metatheoretic propertiesThe progress property and the problem of axioms in type theoryThe progress property and the problem of axioms in type theoryIntroduction to type safetyIntroduction to type safetyIntroduction to metatheoryIntroduction to metatheoryDefinition of the Mendler encodingDefinition of the Mendler encodingThe Mendler encoding and the problem of explicit recursionThe Mendler encoding and the problem of explicit recursionThe Scott encodingThe Scott encodingMore on the Parigot encodingMore on the Parigot encodingIntroduction to the Parigot encodingIntroduction to the Parigot encodingChurch-encoding natural numbersChurch-encoding natural numbersChurch encoding of listsChurch encoding of listsChurch encoding of the booleansChurch encoding of the booleansIntroduction to Church encodingIntroduction to Church encodingFunctional encodings turning the world inside outFunctional encodings turning the world inside outMore benefits of lambda encodingsMore benefits of lambda encodingsIntroduction to lambda encodingsIntroduction to lambda encodingsAdding a top type and allowing non-normalizing termsAdding a top type and allowing non-normalizing termsIntersection types using Curry-style typingIntersection types using Curry-style typingCurry-style versus Church-style, and the nature of type annotationsCurry-style versus Church-style, and the nature of type annotationsMore on Computation First, and Basic Idea of RealizabilityMore on Computation First, and Basic Idea of RealizabilityTypes should be erased for executing and reasoning about programsTypes should be erased for executing and reasoning about programsWhy go beyond GADTs?Why go beyond GADTs?GADTs for programming with representations of typesGADTs for programming with representations of typesUsing GADTs for typed subsetting of your languageUsing GADTs for typed subsetting of your languageExample of programming with indexed types: binary search treesExample of programming with indexed types: binary search treesProgramming with indexed types using singletonsProgramming with indexed types using singletonsLimitations of indexed types that are not truly dependentLimitations of indexed types that are not truly dependentProgramming with Indexed TypesProgramming with Indexed TypesProgram Termination and the Curry-Howard IsomorphismProgram Termination and the Curry-Howard IsomorphismWhy Curry-Howard for classical proofs is a bad idea for programmingWhy Curry-Howard for classical proofs is a bad idea for programmingCurry-Howard for classical logicCurry-Howard for classical logicDependent types and design by contractDependent types and design by contractIndexed types and Curry-Howard for first-order quantifiersIndexed types and Curry-Howard for first-order quantifiersThe Curry-Howard Isomorphism for Propositional LogicThe Curry-Howard Isomorphism for Propositional LogicThe Curry-Howard Isomorphism for InductionThe Curry-Howard Isomorphism for InductionConstructive proofs as programsConstructive proofs as programsIntroduction to the Curry-Howard IsomorphismIntroduction to the Curry-Howard IsomorphismFunctors and catamorphismsFunctors and catamorphismsStructured Recursion Schemes for Point-Free RecursionStructured Recursion Schemes for Point-Free RecursionMore on point-free programming and category theoryMore on point-free programming and category theoryPoint-free programming and category theoryPoint-free programming and category theoryConcise code through point-free programmingConcise code through point-free programmingMore on FP and concise codeMore on FP and concise codeFunctional Programming and Concise Code: Type InferenceFunctional Programming and Concise Code: Type InferenceIntroduction to Functional ProgrammingIntroduction to Functional ProgrammingSoftware Engineering Considerations for Formal MethodsSoftware Engineering Considerations for Formal MethodsPower of Computer-Checked Proofs for SoftwarePower of Computer-Checked Proofs for SoftwareTechnical reasons for lack of adoption of computer-checked proofsTechnical reasons for lack of adoption of computer-checked proofsWhy Computer-Checked Proofs are Not Used More in MathematicsWhy Computer-Checked Proofs are Not Used More in MathematicsComputer-Checked Proofs in American ResearchComputer-Checked Proofs in American ResearchComputer-checked proofs about softwareComputer-checked proofs about softwareMore on Computer-Checked ProofsMore on Computer-Checked ProofsComputer-checked proofsComputer-checked proofs
