A Computer Architect's Attempt at Using Type Theoretic Concepts to Model Branch Predictors

Add to your list(s) Download to your calendar using vCal

• Karl Mose (University of Cambridge)
• Tuesday 06 May 2025, 13:00-14:00
• FS07, Computer Laboratory.

If you have a question about this talk, please contact Ariadne Si Suo .

In this talk, I will introduce PIOUS , a custom domain-specific language I’m developing to describe predictor microarchitectures. I’ll share key design decisions behind the language and reflect on insights I’ve gained about functional programming and type systems during its development, from the perspective of someone who’s not from a type-theoretic background (expect some butchering of terms!). I’ll give a brief overview of branch predictors and cover an earlier attempt to generalise them into a language framework. After discussing the limitations of earlier approaches, I’ll present how PIOUS leverages type systems and the power of indexed monads to describe predictors effectively.

While I’m not from a type theoretic background, this talk should be interesting to those curious about practical applications of type theory to other fields.

This talk is part of the SANDWICH Seminar (Computer Laboratory) series.

This talk is included in these lists:

• FS07, Computer Laboratory
• tcw57’s list

Note that ex-directory lists are not shown.