Does any dialect have formal semantics?

Hi, Sorry I am newbie to MLIR. I am working on a project where I would like to verify the transformations between dialects(existing dialects and my own dialects). I am just wondering is there any formal semantics for the operations in existing dialects, such as linalg? Thanks!

There’s nothing sufficiently formal for Linalg, but we are interested in having something in mid- to long-term.

1 Like