Dependent Types for Formal Theorem Proving: A Case Study of Hall’s Theorem

dc.contributor.advisor	Жежерун, Олександр
dc.contributor.author	Власенко, Павло
dc.date.accessioned	2024-04-04T05:32:05Z
dc.date.available	2024-04-04T05:32:05Z
dc.date.issued	2023
dc.description.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.	uk_UA
dc.identifier.uri	https://ekmair.ukma.edu.ua/handle/123456789/28614
dc.language.iso	en	uk_UA
dc.status	first published	uk_UA
dc.subject	lambda cube	uk_UA
dc.subject	the Curry–Howard isomorphism	uk_UA
dc.subject	simple proofs	uk_UA
dc.subject	Hall’s Marriage Theorem	uk_UA
dc.subject	бакалаврська робота	uk_UA
dc.title	Dependent Types for Formal Theorem Proving: A Case Study of Hall’s Theorem	uk_UA
dc.type	Other	uk_UA

Now showing 1 - 1 of 1