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...
| Main Authors: | , , |
|---|---|
| Other Authors: | |
| Format: | Article |
| Language: | English |
| Published: |
Association for Computing Machinery (ACM)
2019
|
| Online Access: | https://hdl.handle.net/1721.1/121232 |
| _version_ | 1826199812752539648 |
|---|---|
| author | Chlipala, Adam Wang, Peng Want, Di |
| author2 | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory |
| author_facet | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Chlipala, Adam Wang, Peng Want, Di |
| author_sort | Chlipala, Adam |
| collection | MIT |
| description | 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/post-conditions. Indexed types are flexible enough that TiML avoids a built-in notion of "size," and the programmer can choose to index user-defined datatypes in any way that helps her analysis. TiML's distinguishing characteristic is supporting highly automated time-bound verification applicable to data structures with nontrivial invariants. The programmer provides type annotations, and the typechecker generates verification conditions that are discharged by an SMT solver. Type and index inference are supported to lower annotation burden, and, furthermore, big-O complexity can be inferred from recurrences generated during typechecking by a recurrence solver based on heuristic pattern matching (e.g. using the Master Theorem to handle divide-and-conquer-like recurrences). We have evaluated TiML's usability by implementing a broad suite of case-study modules, demonstrating that TiML, though lacking full automation and theoretical completeness, is versatile enough to verify worst-case and/or amortized complexities for algorithms and data structures like classic list operations, merge sort, Dijkstra's shortest-path algorithm, red-black trees, Braun trees, functional queues, and dynamic tables with bounds like m n logn. The learning curve and annotation burden are reasonable, as we argue with empirical results on our case studies. We formalized TiML's type-soundness proof in Coq. |
| first_indexed | 2024-09-23T11:26:27Z |
| format | Article |
| id | mit-1721.1/121232 |
| institution | Massachusetts Institute of Technology |
| language | English |
| last_indexed | 2024-09-23T11:26:27Z |
| publishDate | 2019 |
| publisher | Association for Computing Machinery (ACM) |
| record_format | dspace |
| spelling | mit-1721.1/1212322022-10-01T03:39:44Z TiML: a functional language for practical complexity analysis with invariants Chlipala, Adam Wang, Peng Want, Di Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science 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/post-conditions. Indexed types are flexible enough that TiML avoids a built-in notion of "size," and the programmer can choose to index user-defined datatypes in any way that helps her analysis. TiML's distinguishing characteristic is supporting highly automated time-bound verification applicable to data structures with nontrivial invariants. The programmer provides type annotations, and the typechecker generates verification conditions that are discharged by an SMT solver. Type and index inference are supported to lower annotation burden, and, furthermore, big-O complexity can be inferred from recurrences generated during typechecking by a recurrence solver based on heuristic pattern matching (e.g. using the Master Theorem to handle divide-and-conquer-like recurrences). We have evaluated TiML's usability by implementing a broad suite of case-study modules, demonstrating that TiML, though lacking full automation and theoretical completeness, is versatile enough to verify worst-case and/or amortized complexities for algorithms and data structures like classic list operations, merge sort, Dijkstra's shortest-path algorithm, red-black trees, Braun trees, functional queues, and dynamic tables with bounds like m n logn. The learning curve and annotation burden are reasonable, as we argue with empirical results on our case studies. We formalized TiML's type-soundness proof in Coq. National Science Foundation (U.S.) (Grant CCF-1512611) United States. Defense Advanced Research Projects Agency (FA8750-16-C-0007) 2019-06-10T18:00:00Z 2019-06-10T18:00:00Z 2017-10 2019-05-13T18:00:45Z Article http://purl.org/eprint/type/ConferencePaper 2475-1421 https://hdl.handle.net/1721.1/121232 Wang, Peng, et al. “TiML: A Functional Language for Practical Complexity Analysis with Invariants.” Proceedings of the ACM on Programming Languages 1, OOPSLA, (October 2017): pp. 1–26. © 2017 The Authors en http://dx.doi.org/10.1145/3133903 Proceedings of the ACM on Programming Languages Creative Commons Attribution 4.0 International license https://creativecommons.org/licenses/by/4.0/ application/pdf Association for Computing Machinery (ACM) ACM |
| spellingShingle | Chlipala, Adam Wang, Peng Want, Di TiML: a functional language for practical complexity analysis with invariants |
| title | TiML: a functional language for practical complexity analysis with invariants |
| title_full | TiML: a functional language for practical complexity analysis with invariants |
| title_fullStr | TiML: a functional language for practical complexity analysis with invariants |
| title_full_unstemmed | TiML: a functional language for practical complexity analysis with invariants |
| title_short | TiML: a functional language for practical complexity analysis with invariants |
| title_sort | timl a functional language for practical complexity analysis with invariants |
| url | https://hdl.handle.net/1721.1/121232 |
| work_keys_str_mv | AT chlipalaadam timlafunctionallanguageforpracticalcomplexityanalysiswithinvariants AT wangpeng timlafunctionallanguageforpracticalcomplexityanalysiswithinvariants AT wantdi timlafunctionallanguageforpracticalcomplexityanalysiswithinvariants |