Lean Software Verification
Julian Sutherland ( Nethermind.io )
- 13:00 3rd May 2022 ( Trinity Term 2022 )LTA - Wolfson building Oxford
In this talk, we aim to demonstrate the use of proof assistants in software verification. To this end, will give a practical introduction to dependent types and their use in producing computer checkable proofs. We will then specify the semantics of a simple imperative programming language into the Lean proof assistant (https://leanprover.github.io/) and use it to prove some properties of a simple program.
This talk will be in-person in LTA wolfson building. We will also live stream via Teams using the folowing link
Microsoft Teams meeting
Join on your computer or mobile app