On the 1st of May, we will have a first seminar in our May — June session. We will plan the seminar topics and talks ahead and will welcome new members that joined us since Easter break.
Franta Farka is giving a DREAM talk in Edinburgh University
Franta Farka is giving a talk for the DREAM group at Edinburgh University.
Title: Proof-Relevant Resolution for Constructive Automation.
Venue and time: 23 April, 11:00 , Informatics Forum, room 2.33.
Abstract: In this talk, we introduce proof-relevant resolution, a framework for constructive proof automation. The intended application of the framework is verifiable proof automation in strongly typed programming languages. We motivate the framework by two use-cases that show its strengths. First, we show a proof-relevant approach to type inference and term synthesis. Secondly, we demonstrate the use of the framework for the purpose of study semantical properties of programming languages, namely soundness of type-class elaboration. In the talk, we describe the key features of big-step and small-step operational semantics and show soundness of the small-step w.r.t. the big-step semantics. We briefly outline the proof as it requires a use of logical relation.
Message Input
Daniel Kienitz wins James Watt Scholarship
Our MSc student Daniel Kienitz has just won James Watt PhD Scholarship, that will fund his PhD studies on Verification of Neural Networks. Many congratulations, Daniel, for winning the Scholarship competition, and huge welcome to PhD research team of LAIV!
LAIV papers at ESOP’19 and HCVS’19 at ETAPS next week
Next week, we are presenting our work on Coinduction and Horn clauses at ESOP and HCVS in Prague, both part of the ETAPS, European Joint conference on Theory and Practice of Software.
Daniel, Pascal and Pierre are submitting their MSc reports today: good luck guys and well done for your hard work this term!
LAIV Masterclasses
At the end of March 2019, LAIV will have a marathon of Masterclass presentations by MSc students:
| 18 March | LAIV Masterclass: Survey of Deep Learning: Methods and Applications |
| 21 March | LAIV Masterclass: Convolutional Neural nets |
| 27 March | LAIV Masterclass: Keras and Adversarial example generation |
The LAIV Seminars page holds full details of venues and times.
An academic visitor starting on 11 March
Huge welcome to our new academic visitor, Dmitry Rozplokhas from the Programming Languages and Tools lab, JetBrains. Dmitry is an MSc student at the Higher School of Economics, St Petersburgh and already has a publication at PPDP’18! He will work with us until June 2019 on the topic of coinduction in relational programming. Welcome to LAIV members, Dmitry!
Next SPLS, 13 March
The next Scottish Programming Language Seminar will be held at St Andrews University, on 13th March: https://eb.host.cs.st-andrews.ac.uk/SPLS-Feb19/
Launch of LAIV webpage
We are launching the webpage of the newly opened Lab for AI and Verification (LAIV): laiv.uk