Abstract:
|
We present F^, a lambda calculus for which termination is guaranteed by the typing rules and show some ideas used to design an inference algorithm for it. F^ (read as F sombrero) results from enriching Girard's system F with size annotations. This allows constructor depth to be bounded, making it possible to guarantee strong normalization of well typable expressions. This property together with a type inference algorithm, allows static verification of many terminating programs. More importantly, it guarantees correctness of "inductive" proofs in logical systems based on the Curry-Howard isomorphism. |