Seen on Lambda the Ultimate: Gradual Typing for Functional Languages, a paper that introduces a new flavor of lambda calculus which they call (this is an approximation) λ?→.
Hard to explain why language geeks should be excited about this. I am.
We present a formal type system that supports gradual typing for functional languages, providing the flexibility of dynamically typed languages when type annotations are omitted by the programmer and providing the benefits of static checking when function parameters are annotated.
The proofs in the paper are machine-verified!
No comments:
Post a Comment