fixes, add OCaml Light definition pdf

index.html

@@ -81,8 +81,12 @@ <h2 id="seminar-slides">Seminar Slides</h2>
 <li><a href="ott/lamtyp.pdf">simply typed lambda calculus pdf</a></li>
 <li><a href="ott/lamtypbool.ott">simply typed lambda calculus with Booleans Ott file</a></li>
 <li><a href="ott/lamtypbool.pdf">simply typed lambda calculus with Booleans pdf</a></li>
-<li><a href="https://softwarefoundations.cis.upenn.edu/plf-%20current/Stlc.html">Definition of STLC</a> in Software Foundations book by Pierce et al.</li>
-<li><a href="https://softwarefoundations.cis.upenn.edu/plf-%20current/StlcProp.html">Properties of STLC</a> in Software Foundations book by Pierce et al.</li>
+<li><a href="https://softwarefoundations.cis.upenn.edu/plf-current/Stlc.html">Definition of STLC</a> in Software Foundations book by Pierce et al.</li>
+<li><a href="https://softwarefoundations.cis.upenn.edu/plf-current/StlcProp.html">Properties of STLC</a> in Software Foundations book by Pierce et al.</li>
+<li><a href="https://citeseerx.ist.psu.edu/doc/10.1.1.107.7364">Research paper on OCaml Light</a></li>
+<li><a href="ott/caml_typedef.pdf">Full definition of OCaml Light</a>, see also the <a href="https://github.com/ott-lang/ott/tree/master/examples/ocaml_light">Ott repository</a></li>
+<li><a href="https://cakeml.org/ifl15.pdf">Research paper on the CakeML</a></li>
+<li><a href="https://gist.github.com/palmskog/a988783a000ae6319eed15819eeb60ac">Example CakeML program</a> (proof checker for propositional logic proofs)</li>
 </ul>
 </td>
 </tr>