Жежерун, ОлександрВласенко, Павло2024-04-042024-04-042023https://ekmair.ukma.edu.ua/handle/123456789/28614This 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.enlambda cubethe Curry–Howard isomorphismsimple proofsHall’s Marriage Theoremбакалаврська роботаOther