Loading...
semester or other student projects
Formal foundations for GADTs in Scala
April 17, 2020
GADTs are a very useful language feature that allow encoding some invariants in types. GADT reasoning is currently implemented in Scala and Dotty, but it’s plagued with soundness issues. To get a better understanding of GADTs in Scala, we explore how they can be encoded in pDOT, a calculus that is the formal foundation of the Scala programming language, and show a sketch of encoding a calculus containing GADTs to pDOT.
Loading...
Name
Formal foundations for GADTs in Scala.pdf
Type
Preprint
Access type
openaccess
Size
194.58 KB
Format
Adobe PDF
Checksum (MD5)
637fd1dad3735072533cccc03466ffa3