TiML: a functional language for practical complexity analysis with invariants

We present TiML (Timed ML), an ML-like functional language with time-complexity annotations in types. It uses indexed types to express sizes of data structures and upper bounds on running time of functions; and refinement kinds to constrain these indices, expressing data-structure invariants and pre...

Full description

Bibliographic Details
Main Authors: Chlipala, Adam, Wang, Peng, Want, Di
Other Authors: Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory
Format: Article
Language:English
Published: Association for Computing Machinery (ACM) 2019
Online Access:https://hdl.handle.net/1721.1/121232