2026-spring-summer

Speaker	Time ∧ Location	Paper
	Abstract
Matthew Keenan	June 25th, 10-11:30am@4901 BBB	Isabelle: The next 700 theorem provers
	We'll take a look at the design and history of the Isabelle proof assistant, how its philosophy differs to that of rocq/lean, what it's strengths are, and why it never quite got the hype.
Thomas Porter	June 11th, 10-11:30am@4901 BBB	Design and Implementation of the Andromeda Proof Assistant
	Andromeda is an LCF-style proof assistant where the user builds derivable judgments by writing code in a meta-level programming language AML. The only trusted component of Andromeda is a minimalist nucleus (an implementation of the inference rules of an object-level type theory), which controls construction and decomposition of type-theoretic judgments. Since the nucleus does not perform complex tasks like equality checking beyond syntactic equality, this responsibility is delegated to the user, who implements one or more equality checking procedures in the meta-language. The AML interpreter requests witnesses of equality from user code using the mechanism of algebraic operations and handlers. Dynamic checks in the nucleus guarantee that no invalid object-level derivations can be constructed. To demonstrate the flexibility of this system structure, we implemented a nucleus consisting of dependent type theory with equality reflection. Equality reflection provides a very high level of expressiveness, as it allows the user to add new judgmental equalities, but it also destroys desirable meta-theoretic properties of type theory (such as decidability and strong normalization). The power of effects and handlers in AML is demonstrated by a standard library that provides default algorithms for equality checking, computation of normal forms, and implicit argument filling. Users can extend these new algorithms by providing local "hints" or by completely replacing these algorithms for particular developments. We demonstrate the resulting system by showing how to axiomatize and compute with natural numbers, by axiomatizing the untyped lambda-calculus, and by implementing a simple automated system for managing a universe of types.

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.