<html><head></head><body><div style="font-family:Helvetica Neue, Helvetica, Arial, sans-serif;font-size:13px;"><div id="ydpe4846f21yiv8101917895"><!--[if gte mso 9]><xml><o:OfficeDocumentSettings><o:AllowPNG/><o:PixelsPerInch>96</o:PixelsPerInch></o:OfficeDocumentSettings></xml><![endif]--><div><div style="font-family:Helvetica Neue, Helvetica, Arial, sans-serif;font-size:13px;"><div>Hello folks:</div><div>I admire you too much because keep my learning and what a surprise, the underlying theory of JVM verifier in its latest version, (in the sense of bytecode verifier, not JVM architecture exerciser which AFAIK is proprietary, but heck we have VAX one) is derived from Cardelli/Nelson veneer (with Cardelli-Abadi seminal work on Baby Modula-3 and a Theory of objects as Nelson/George Necula Peter Lee Proof Carrying code).</div><div>As I understand these type systems are so solid and strong that you can prove besides programs don't go wrong many more properties than simpler systems can, e.g security. See [1]:</div><div><a href="https://docs.oracle.com/javase/specs/jvms/se7/html/jvms-0-preface7.html" rel="nofollow" target="_blank">https://docs.oracle.com/javase/specs/jvms/se7/html/jvms-0-preface7.html</a><div><br></div><div>Keep the language alive folks<br></div><div><br></div><div><div class="ydpe93ab555csl-bib-body" style="line-height: 1.35; ">
<div class="ydpe93ab555csl-entry" style="clear: left; "><br>[1] «CiteSeerX — Towards Secure Bytecode Verification on a Java Card». [On line]. Available on: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.50.4920. [Accesed: 13-oct-2017].<br><br><br></div>
<span class="ydpe93ab555Z3988" title="url_ver=Z39.88-2004&ctx_ver=Z39.88-2004&rfr_id=info%3Asid%2Fzotero.org%3A2&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Adc&rft.type=webpage&rft.title=CiteSeerX%20%E2%80%94%20Towards%20Secure%20Bytecode%20Verification%20on%20a%20Java%20Card&rft.identifier=http%3A%2F%2Fciteseerx.ist.psu.edu%2Fviewdoc%2Fsummary%3Fdoi%3D10.1.1.50.4920"></span>
</div><br></div><br></div></div></div></div></div></body></html>