X-Git-Url: https://git.ralfj.de/web.git/blobdiff_plain/a859220c739395803573893936de9e11da335e64..47a72d30696caed054fe475de3c6c5287f8863aa:/ralf/_posts/2019-10-20-type-soundness.md

diff --git a/ralf/_posts/2019-10-20-type-soundness.md b/ralf/_posts/2019-10-20-type-soundness.md
new file mode 100644
index 0000000..a8b9dbb
--- /dev/null
+++ b/ralf/_posts/2019-10-20-type-soundness.md
@@ -0,0 +1,14 @@
+---
+title: 'What Type Soundness Theorem Do You Really Want to Prove?'
+categories: rust research
+---
+
+My advisor Derek and some of my coauthors Amin, Robbert and Lars just put out a blog post on the [SIGPLAN blog](https://blog.sigplan.org/) on the idea of "semantic typing".
+This is the methodology behind [RustBelt](https://plv.mpi-sws.org/rustbelt/popl18/), so the post is a great starting point for understanding the context of that paper and the key bits of prior research that it rests on.
+In fact they used Rust as their main example language for that post, and I helped them out a bit with some of the technical details there so they kindly added me to the author list.
+
+The approach they describe is much more widely applicable than Rust though; it provides a whole new perspective on type systems that I think deserves way more attention than it gets.
+If you are interested in formal methods for type systems and in particular for Rust, you should check it out!
+It's a great read:
+
+> ["What Type Soundness Theorem Do You Really Want to Prove?" on *PL Perspectives*](https://blog.sigplan.org/2019/10/17/what-type-soundness-theorem-do-you-really-want-to-prove/)