Mediaspace scheduled maintenance: Aug 25, 2026 07:00 - 12:00 AM. During this time, videos will be temporarily unavailable. Check status updates.

Type theory

Related lectures (32)

Dependent Types in Programming Languages

Explores maps, type operators, equivalence, first-class types, System Fw, Coq, and the challenges of type checking in programming languages.

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.

Type Checking and Reconstruction: Equations and Unification

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

Lambda Calculus: Syntax and Abstractions

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

Types in Lambda Calculus

Covers types in lambda calculus, including defining types, specifying rules, and proving soundness.

Coq Workshop: Introduction to Interactive Theorem Proving

Introduces Coq, an interactive theorem assistant based on the Curry-Howard isomorphism.

Verifying Programs with Stainless: How Stainless Works

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

Church Numerals and Conditionals

Explores Church numerals and encoding conditionals in lambda calculus.

Lambda Calculus: Church Numerals

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

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.

Foundations of Scala: Modelling and Type Systems

Covers the foundations of Scala, including modelling recursive types, parameterized types, and variance.

Lambda Calculus: Operational Semantics and Evaluation Strategies

Covers operational semantics and evaluation strategies in lambda calculus, including redex, alternative evaluation strategies, and Church Booleans.

Coq Workshop: Inductive Data Types and Proofs

Covers the definition of an inductive data type in Coq and how to build proofs interactively using tactics.

Semantics in Computer Language Processing: Understanding Meaning

Covers the semantics of programming languages, focusing on the Add language and the role of rewriting rules and CK machines in understanding meaning.

Encoding Recursion as Self-Application

Explores lambda calculus, higher-order functions, and recursive function encoding.

Coq: Overview

Introduces Coq and focuses on proving the theorem and_comm step by step.

Covers self-similar groups and automorphisms of rooted trees, exploring residually finite groups and congruence subgroups.

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.

Multi-Regional Input Output Analysis: EXIOBASE 3

Covers the computation of Economy-Wide Material Flow Analysis for Switzerland using EXIOBASE 3.