"an intriniscally-typed formalisation of WebAssembly in Agda"
đź‘€ @me
@ltchen @gallais @me The current formalisation is extrinsically typed, meaning the evaluator has to explicitly prove each step is well-typed. With intrinsic typing you basically get this part for free, which can lead to things being cleaner (but this is somewhat subjective)
With that said I've been procrastinating finishing this for a while, and in the meantime wasm & spectec have moved a lot, so this is more of a hobby project.