- </ul>
- <ul id="static">
- <li>
- <a href="http://lambdadelta.info/static/matita/lambdadelta/">lambdadelta_1 for Matita 0.5"</a>
- (revised <span class="date">2011-09</span>).
- Static HTML pages generated by the <a href="http://helm.cs.unibo.it/">HELM</a> rendering engine.
- <ul>
- <li>
- <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/pr3/pr3/pr3_confluence.con.html">
- Confluence of reduction</a>
- (Church-Rosser property).
- </li>
- <li>
- <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/props/ty3_correct.con.html">
- Correctness of types</a>.
- </li>
- <li>
- <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/props/ty3_unique.con.html">
- Uniqueness of types up to conversion</a>.
- </li>
- <li>
- <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/pr3/ty3_sred_pr3.con.html">
- Subject reduction of the type assignment</a>.
- </li>
- <li>
- <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/arity_props/ty3_sn3.con.html">
- Strong normalization of the typed terms</a>.
- </li>
- <li>
- <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/dec/ty3_inference.con.html">
- Decidability of the type inference problem</a>.
- </li>
- </ul>
+ <li>
+ <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/props/ty3_correct.con.html">
+ Correctness of types</a>.