Compile-Time Dependent Types

Syl is a new programming language under development that encodes compile-time computation in a modal type system, using two mode axes: staticity and erasure.