School of Mathematics

Four and a half proofs of a product-measure version of the Erdös-Ko-Rado Theorem.

Ehud Friedgut
The Weizmann Institute of Science
September 24, 2018

The EKR theorem, which is the cornerstone of extremal combinatorics, characterizes maximal intersecting families of sets. Its setting fixes a ground set of size n, and then studies the size and structure of intersecting families of subsets of fixed size k. A setting which many might consider no less natural, is considering the Boolean lattice of all subsets of {1,...,n} endowed with a product measure, and studying the structure and measure of maximal intersecting families.

Univalence from a computer science point-of-view

Dan Licata
Wesleyan University
September 14, 2018
Abstract: One formal system for Voevodsky's univalent foundations is Martin-Löf's type theory. This type theory is the basis of proof assistants, such as Agda, Coq, and NuPRL, that are used not only for the formalization of mathematics, but in computer science for verification of programs, systems, and programming language designs and implementations. These applications rely on the fact that constructions in type theory can be interpreted constructively as programs.