Lectures related to Types in Lambda Calculus

Type Checking and Reconstruction: Equations and Unification

Delves into type checking, reconstruction, equations, unification, Hindley/Milner system, polymorphism, and principal types.

Verified Functional Programming: Nicolas Voirol public PhD thesis defense

Explores verified functional programming, formal verification, SMT solvers, type checking, Scala features, automation, and dependent types.

Lambda Calculus: Church Numerals

Explores Church numerals, Booleans, pairs, recursion, and behavioral equivalence in Lambda Calculus.

Type Systems: Preservation and Typing Rules

Covers preservation, substitution, weakening, and sequencing in type systems.

Logical Formulas and Types: Understanding the Kerry Howard Isomorphism

Explores the Kerry Howard Isomorphism, translating logical propositions into types and terms, with a focus on proof by induction and exam preparation.

Python Programming Basics

Covers the basics of Python programming, focusing on flow control structures, interactive mode, script mode, and variables.

Boolean Types and Control Structures

Explores boolean types, logical operators, and control structures in Python, emphasizing the evaluation of expressions and the use of relational operators.

Lambda Calculus: Syntax and Abstractions

Introduces terms, abstractions, applications, and values in the lambda calculus.

Verifying Compiler: Spec# Approach

Explores the Spec# programming system, focusing on a verifying compiler for C# 2.0.

Subtyping and Polymorphism

Explores subtyping rules, challenges, and its connection to various forms of polymorphism in programming languages.

Class hierarchies: pattern matching

Covers class hierarchies, pattern matching, function values, and function calls in Scala.

Verifying Programs with Stainless: How Stainless Works

Explores the inner workings of the Stainless framework, emphasizing verification-aware transformations and dependent type checking.

Designing Learning Experiences: CS411 Class Project

Introduces the CS411 Class Project, where students design and test a lesson using learning theories.

Records and Variants

Introduces records, variants, evaluation rules, typing rules, aliasing challenges, and benefits in programming languages.

Type Rules: Progress, Preservation

Covers type rules, program type checking, soundness, and proof techniques.

Lambda Calculus and Type Safety: An Overview Log in to Mediaspace to watch this video

Provides an overview of lambda calculus, type safety, and type inference in programming languages.

Simply Typed Lambda Calculus: Foundations and Properties Log in to Mediaspace to watch this video

Covers the simply typed lambda calculus, focusing on its syntax, semantics, and type system properties such as progress and preservation.

Stochastic Endowment Consumption Model Log in to Mediaspace to watch this video

Covers the stochastic endowment consumption model, log-linear transformation, impulse response solution, and Matlab codes.

Python Programming: List Comprehensions and Higher Order Functions Log in to Mediaspace to watch this video

Explores advanced Python programming concepts, focusing on list comprehensions and higher order functions.

Block Pulled by a Spring Log in to Mediaspace to watch this video

Explores the dynamics of a block pulled by a spring under various conditions.