Seminars

As compute systems become increasingly heterogeneous and specialized, compiler infrastructure is no longer just a way to generate code—it can be a practical tool to shape hardware design decisions, tighten end-to-end design cycles, and share the verification burden.

As compute systems become increasingly heterogeneous and specialized, compiler infrastructure is no longer just a way to generate code—it can be a practical tool to shape hardware design decisions, tighten end-to-end design cycles, and share the verification burden.

Lean is a proof assistant developed by the Lean FRO that has become especially popular with mathematicians in recent years, whose type-theoretic foundations take after the proof assistant Rocq.

*Abstract*

Speaker:
Andrey Breslav is the creator of the Kotlin programming language and led its development at JetBrains from its inception to millions of users worldwide. He is the founder of CodeSpeak.dev, a next-generation programming language powered by large language models (LLMs).

This paper is published this week in Quantum at https://doi.org/10.22331/q-2026-01-19-1972

Recent progress in language models and artificial agents has renewed foundational questions about how intelligence is learned, structured and represented. In this omnibus talk, I present three complementary perspectives on these questions.

Foundation models are transforming structured data learning much like large language models did for text.

Abstract: Homotopy Type Theory (HoTT) is a new field of research combining constructive type theory, homotopy theory, and higher category theory, with applications to the formalization of mathematics.