Events: Data- och informationsteknikhttp://www.chalmers.se/sv/om-chalmers/kalendariumUpcoming events at Chalmers University of TechnologyThu, 29 Jun 2017 13:44:25 +0200http://www.chalmers.se/sv/om-chalmers/kalendariumhttp://www.chalmers.se/en/departments/cse/calendar/Pages/magnusmyreendocent.aspxhttp://www.chalmers.se/en/departments/cse/calendar/Pages/magnusmyreendocent.aspxFormal verification: from machine code to functional programming<p>EA, lecture hall, EDIT trappa C, D och H, EDIT</p><p>​Docent lecture by Magnus Myreen.</p>​<img src="/SiteCollectionImages/Institutioner/DoIT/Profile%20pictures/ST/Myreen.gif" class="chalmersPosition-FloatRight" alt="" style="margin:5px" />ABSTRACT <br />This talk will describe how my research on formal verification has moved between verification of low-level machine code and high-level functional programming. I will focus on my work on an end-to-end correctness theorem for a reflective theorem prover for a Lisp-like logic. I describe the theorem as an &quot;end-to-end&quot; result because it relates the execution of something low level (in this case: a machine-code implementation of Lisp) with a high-level property of the running application (in this case: logical soundness of the hosted Lisp theorem prover). My collaborator and I proved that the Lisp theorem prover can only prove logically sound statements when run on our verified implementation of Lisp. <br /><br />Although I have finished working on Lisp, I have chosen to talk about this line of work because I see it as the motivation and blueprint for my current work on CakeML (<a href="https://cakeml.org/">https://cakeml.org/</a>). <br /><br />My work is in the context of mechanised theorem proving using the interactive HOL theorem prover <br />(<a href="https://hol-theorem-prover.org/">https://hol-theorem-prover.org/</a>). http://www.chalmers.se/en/areas-of-advance/ict/calendar/Pages/ACM-VRST-2017.aspxhttp://www.chalmers.se/en/areas-of-advance/ict/calendar/Pages/ACM-VRST-2017.aspxThe ACM Symposium on Virtual Reality Software and Technology (VRST) 2017<p>Chalmers Lindholmen, Gothenburg</p><p>​VRST will provide an opportunity for VR researchers to interact, share new results, show live demonstrations of their work, and discuss emerging directions for the field.</p>​ <br />The ACM Symposium on Virtual Reality Software and Technology (VRST) is an international forum for the exchange of experience and knowledge among researchers and developers concerned with virtual reality software and technology. <br /><br /><a href="https://vrst.acm.org/vrst2017/index.html">To conference website: http://vrst.acm.org/vrst2017/</a><br /><br />