LAIV team is attending next SPLS in Edinburgh, 17th June: https://spls-series.github.io/meetings/2019/june/

Many congratulations to LAIV MSc student Pierre Le Hen who secured a place to do a Masters specialising in Management of Systems Information at ESSEC: http://www.essec.edu/fr/programme/masters/mastere-specialise-management-des-systemes-dinformation-en-reseaux/admission/

The positions are highly competitive, so well done Pierre and hope you have a great career ahead of you!

The Second Big Proof event has started today in Edinburgh, following its first edition at Cambridge in 2017. A number of LAIV members are participating, Katya is giving a talk on LAIV’s experience in Neural net verification.

First Scottish Summer School on Programming Languages and Verification is now announced. LAIV supported this initiative in a number of ways: Katya Komendantskaya serves in the steering committee as one of the main organisers, and Rob Stewart is going to give a course on Domain Specific Languages. This school is highly recommended to all PhD students, as well as strong MSc students and Early Career researchers. Industrial participants and sponsors are very welcome.

LAIV students start a reading group on Software Foundations in Coq, https://softwarefoundations.cis.upenn.edu/ The reading and programming sessions will take place every Tuesday at 10.00. Check-out the schedule and room changes at https://github.com/laiv-research/SoftwareFoundations or email Daniel Kienitz directly.

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 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

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!

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.