Michael Pellauer

I'm a grad student in Computer Science at MIT. My research interests include semantics of computer architecture, processor modelling, functional programming, and formal verification. Much of my work is done in Bluespec or Haskell.

What is semantics of computer architecture?

Traditionally the field of semantics asks questions like "What does program A mean?" and "Is Program A equivalent to Program B?"

In semantics of architecture we ask questions like "What does program A mean on architecture P?" or "What is the language of programs that architecture P provides?" or most importantly "Is architecture P equivalent to architecture Q?"

This forces us to rethink many notions of equivalence. For example consider two programs A and B, where both calculate the same result but A does so in 10 clock cycles, while B takes 10 years. Traditional semantics would say that these are equivalent, but if we are trying to use our semantic model to automatically optimize an architecture then perhaps we should reconsider. An open question is whether such parameters as execution time, resource utilization or power consumption should be considered constraints or fundamental considerations in the semantic model.

Educational Background


1999 Brown University
Providence, RI
Double B.A. in Computer Science and English
magna cum laude


2003 Chalmers University of Technology
Gothenburg, Sweden
M.Sc. in Dependable Computing Systems
Master's Thesis: CoreLoom: A Semantic Model for Fine-Grained Flexible Datapaths
Thesis Advisor: John Hughes, through the FlexSoC project