Dependent Types for Formal Theorem Proving: A Case Study of Hall’s Theorem
Loading...
Date
2023
Authors
Власенко, Павло
Journal Title
Journal ISSN
Volume Title
Publisher
Abstract
This thesis investigates the role of dependent types and Curry-Howard isomorphism in formal theorem proving and programming. First, we highlight the connection between formal logic and type theory and demonstrate how dependent types allow us to encode complex properties like proofs or programs. Next, we introduce Lean, a language utilizing dependent types, and show practical examples to check that the program will never fail and be correct at compile time without needing tests. Finally, we will show an example of a more complex theorem defined in Lean – Hall’s graph theorem and how to use its proof to write the verified program.
Description
Keywords
lambda cube, the Curry–Howard isomorphism, simple proofs, Hall’s Marriage Theorem, бакалаврська робота