2026-winter

Speaker	Time ∧ Location	Paper
	Abstract
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.