2026-winter

Speaker	Time ∧ Location	Paper
	Abstract
Alexander Bandukwala	April 9th, 10-11:30am@4901 BBB	Unison: yesterday's tomorrow, today
	Unison is a statically-typed, functional programming language that takes a fundamentally different approach to code organization by storing programs in a database rather than as text files. Its most distinctive innovation is content-addressed code — using hashes instead of names for references — which eliminates an entire class of dependency conflicts. The language also introduces "abilities" for effect handling, enabling elegant distributed programming where computations can be seamlessly moved across network boundaries with automatic dependency deployment. Unison supports live refactoring with continuous typechecking and direct value serialization, fundamentally rethinking how modern software development workflows operate.
Steven Schaefer	January 15th, 10-11:30am@4901 BBB	Controlling unfolding in type theory
	We present a new way to control the unfolding of definitions in dependent type theory. Traditionally, proof assistants require users to fix whether each definition will or will not be unfolded in the remainder of a development; unfolding definitions is often necessary in order to reason about them, but an excess of unfolding can result in brittle proofs and intractably large proof goals. In our system, definitions are by default not unfolded, but users can selectively unfold them in a local manner. We justify our mechanism by means of elaboration to a core theory with extension types -- a connective first introduced in the context of homotopy type theory -- and by establishing a normalization theorem for our core calculus. We have implemented controlled unfolding in the cooltt proof assistant, inspiring an independent implementation in Agda.