PL Notation is a Barrier to Entry
Research in programming languages offers powerful tools, but our systems of notation stymie outsiders. Can we change our notational approach and broaden our audience—without compromising on content?
Archive of posts tagged: type system
What Type Soundness Theorem Do You Really Want to Prove?
For decades, researchers have syntactically proved type soundness to establish their type system works. This post shows why a semantic notion of type soundness is more appropriate, for covering abstraction and unsafe features.
