LAIV students start a reading group on Software Foundations

LAIV students start a reading group on Software Foundations in Coq, The reading and programming sessions will take place every Tuesday at 10.00. Check-out the schedule and room changes at or email Daniel Kienitz directly.

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 Masterclasses

At the end of March 2019, LAIV will have a marathon of Masterclass presentations by MSc students:

18 MarchLAIV Masterclass: Survey of Deep Learning: Methods and Applications
21 MarchLAIV Masterclass: Convolutional Neural nets
27 MarchLAIV Masterclass: Keras and Adversarial example generation

The LAIV Seminars page holds full details of venues and times.