The following summary was generated by AI from the slides.
TiML (OOPSLA 2017, by Peng Wang, Di Wang, and Adam Chlipala) is a functional language extending System with indexed types and refinement kinds that enables practical worst-case time-complexity verification with user-defined size measures and data-structure invariants. Function types carry cost-bound index annotations (e.g., ), Big-O complexity classes are expressed as refinement kinds (e.g., ), and all verification conditions over index expressions are discharged automatically by an SMT solver. The system is evaluated on 17 benchmark programs including mergesort, red-black tree operations, and foldl, with a Coq-formalized soundness proof via fuel-augmented semantics guaranteeing that well-typed programs never exhaust their stated cost bound.