Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
The goal of the TIL project was to explore the use of Typed Intermediate Languages to produce high-performance native code from Standard ML (SML). We believed that existing compilers, such as Standard ML of New Jersey (SML/NJ), were doing a good job of conventional functional language optimizatons, as one might find in a LISP compiler, but that inadequate use was made of the rich type information present in the source language. Our goal was to show that we could achieve much greater performance by propagating type information through to the back end of the compiler, without sacrificing the advantages afforded by loop-oriented and other optimizations. We also confirmed that using typed intermediate languages dramatically improved the reliability and maintainability of the compiler itself. In particular, we were able to use the type system to express critical invariants, and enforce those invariants through type-checking. In this respect, TIL introduced and popularized the notion of a certifying compiler, which attaches a checkable certificate of safety to its generated code. In turn, this led directly to the idea of certified object code, inspiring the development of Proof-Carrying Code and Typed Assembly Language as certified object code formats.