Hausdorff Center for Mathematics Courses

Erik Palmgren: From Type Theory to Setoids and Back

Exploring setoids in constructive mathematics, their implementation in proof assistants, and their role in formalizing Bishop-style mathematics and Martin-Löf type theory models.

• YouTube
• 1 hour 6 minutes
• Self-Paced
• Free Video

Giovanni Sambin - Pointfree Topology Is Real and Pointwise Is Ideal

Explore dynamic perspectives in mathematics, blending computation and spatial intuition. Learn about positive topology, effective pointfree approaches, and the balance between real and ideal mathematical concepts.

• YouTube
• 1 hour 4 minutes
• Self-Paced
• Free Video

Notions of Booleanization in Pointfree Topology

Explores overlap algebras as a potential solution to retain features of Boolean locales while recovering classical properties in intuitionistic pointfree topology.

• YouTube
• 34 minutes
• Self-Paced
• Free Video

Two Constructive Approaches to Probability Theory

Explores constructive approaches to probability theory, comparing frequentist and pointfree metric methods with classical Kolmogorov axioms and other paradigms in mathematics.

• YouTube
• 34 minutes
• Self-Paced
• Free Video

Iosif Petrakis - Bishop Spaces and the Problem of Constructivizing General Topology

Explores Bishop spaces as a constructive alternative to classical topology, overcoming obstacles in continuity and compactness. Presents key results and connections to other constructive space notions.

• YouTube
• 34 minutes
• Self-Paced
• Free Video

Algorithms for Computing Syzygies Over VX 1, …, X N, V a Valuation Ring

Explore algorithms for computing syzygies in polynomial rings over valuation domains, focusing on a general method without Gröbner bases and its combinatorial termination proof.

• YouTube
• 1 hour
• Self-Paced
• Free Video

Douglas Bridges - Ishihara’s Contributions to Constructive Analysis

Explore Ishihara's key contributions to constructive analysis, including tricks, principles, and theorems, with insights on their impact and applications in mathematical reasoning.

• YouTube
• 45 minutes
• Self-Paced
• Free Video

Every Metric Space Is Separable in Function Realizability

Explore function realizability topos, separable metric spaces, and countable objects with decidable equality. Delve into synthetic topology and its implications for intuitionistic logic.

• YouTube
• 33 minutes
• Self-Paced
• Free Video

Constructive Mathematics in Univalent Type Theory

Explore constructive mathematics within univalent type theory, delving into advanced concepts and their applications in modern mathematical foundations.

• YouTube
• 1 hour
• Self-Paced
• Free Video

Derived Rules in Set Theory

Explore intuitionistic set theories and learn about a general machinery for demonstrating derived rules in this advanced mathematical lecture.

• YouTube
• 42 minutes
• Self-Paced
• Free Video

Triposes and Gödel's Dialectica Interpretation

Exploring semantic presentation of Gödel's Dialectica interpretation using triposes, addressing previous work and suggesting solutions to related questions in mathematical logic.

• YouTube
• 30 minutes
• Self-Paced
• Free Video

Two Observations on Intuitionistic Logic and Arithmetic

Explore intuitionistic logic and arithmetic through finite type formalisation and negative translations. Gain insights into extensional and intensional models, decidable atomic formulas, and equality at higher types.

• YouTube
• 36 minutes
• Self-Paced
• Free Video

Refinement Type Systems and Martin Lof Type Theory

Explores refinement type systems, their connection to Martin-Lof type theory, and various notions of comprehension. Discusses recent work on functors as type refinement systems and Isbell duality theorem.

• YouTube
• 1 hour 1 minute
• Self-Paced
• Free Video

An Introduction to Tensorial Logic and Dialogue Categories

An introduction to tensorial logic, exploring its relationship with dialogue games and categories. Refines linear logic and provides insights into dialogical interpretations of proofs and programs.

• YouTube
• 33 minutes
• Self-Paced
• Free Video

On B-adic Representation of Irrational Numbers

Explore b-adic representation of irrational numbers with Lars Kristiansen, delving into advanced mathematical concepts and their applications in number theory and analysis.

• YouTube
• 37 minutes
• Self-Paced
• Free Video