Yjthnc6htxpfo0hlnvg9
SkillsCast

Lightning Talk: Proving your Haskell Code Correct with Lean

11th October 2018 in London at CodeNode

There are 38 other SkillsCasts available from Haskell eXchange 2018

Please log in to watch this conference skillscast.

Https s3.amazonaws.com prod.tracker2 resource 41088130 skillsmatter conference skillscast o9nohu

Lean is a theorem prover that supports core Haskell features like type classes and monads, and also lots of goodies like dependent types and tactics for proof automation. In this talk Robin will demo using Lean to prove that some functional code always obeys a specification, using more or less just secondary-school level mathematics.

YOU MAY ALSO LIKE:

Thanks to our sponsors

Lightning Talk: Proving your Haskell Code Correct with Lean

Robin Green

Robin Green is a programmer with a long-standing interest in functional programming and formal verification. He started programming in Basic as a child in the 1980s and worked his way up to programming in proof assistants. He has a BSc in Computer Science, Mathematics and Independent Studies from Lancaster University, and an MSc in Computer Science from UCD Dublin. His thesis title was "Verified Monadic Programming".

SkillsCast

Please log in to watch this conference skillscast.

Https s3.amazonaws.com prod.tracker2 resource 41088130 skillsmatter conference skillscast o9nohu

Lean is a theorem prover that supports core Haskell features like type classes and monads, and also lots of goodies like dependent types and tactics for proof automation. In this talk Robin will demo using Lean to prove that some functional code always obeys a specification, using more or less just secondary-school level mathematics.

YOU MAY ALSO LIKE:

Thanks to our sponsors

About the Speaker

Lightning Talk: Proving your Haskell Code Correct with Lean

Robin Green

Robin Green is a programmer with a long-standing interest in functional programming and formal verification. He started programming in Basic as a child in the 1980s and worked his way up to programming in proof assistants. He has a BSc in Computer Science, Mathematics and Independent Studies from Lancaster University, and an MSc in Computer Science from UCD Dublin. His thesis title was "Verified Monadic Programming".

Photos