TiML: A Functional Programming Language with Time Complexity (Parser, Typechecker and Coq Formalization)
Install SML/NJ. Make sure command
ml-buildis in current PATH. On Ubuntu, use this command to install all necessary components of SML/NJ:
sudo apt-get install smlnj libsmlnj-smlnj ml-yacc ml-ulex
Install the Z3 SMT solver version 4.4.1. Make sure command
z3is in current PATH. Z3-4.4.1 is required. Z3-4.4.2 has a known issue.
Install Ruby. Make sure command
rubyis in current PATH.
maketo build TiML, or use
./test.shto build and test on files in examples sub-directory.
(Optional). Install MLton (a whole-program optimizing SML compiler). Make sure command
mllexis in current PATH. Use
make mltonto build TiML with MLton, or use
./test-mlton.shto build and test on files in examples sub-directory.
(Optional, requires step 5). Run
ruby benchmark.rbin directory examples, which will generate file
result.csvthat reproduces results in Table 1 of the paper.
(Optional). Follow emacs/README.rst to install TiML mode on Emacs.
Play with TiML
examples/test-suite.pkg lists all the benchmark examples. You can use this command to run all the examples:
./main.sh examples/stdlib.pkg examples/test-suite.pkg
or this command to run a single example:
./main.sh examples/stdlib.pkg examples/FILENAME.timl
Note that examples/stdlib.pkg (the standard library) is usually needed.
Readers are advised to read the example files following the order in Table 1 of the companion paper (and in file examples/test-suite.pkg), as new syntax are explained in that order.
To reproduce the results in Table 1 of the companion paper, you can run
cd examples ruby benchmark.rb
The results will be printed out and written to file "result.csv". Note that this experiment requires MLton, and your processing time may vary.
The Coq formalization of TiML and its soundness is in proof/Soundness.v. The proof requires Coq 8.5pl3. To check the proof, first compile the utility library:
You can also compile the utility library and the soundness proof altogether: