<div class="csl-bib-body">
<div class="csl-entry">Wiesnet, F. (2025, June 13). <i>Efficient Program Extraction in Elementary Number Theory using the Proof Assistant Minlog</i> [Conference Presentation]. TYPES 2025, University of Strathclyde, United Kingdom of Great Britain and Northern Ireland (the). http://hdl.handle.net/20.500.12708/223818</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/223818
-
dc.description.abstract
We examine theorems of elementary number theory using a constructive, computational, and proof-theoretic approach. Key theorems include Euclid’s proof of the infinitude
of prime numbers, Bézout’s identity, the Fundamental Theorem of Arithmetic, and Fermat’s factorization method. These theorems have been formalized within the proof assistant Minlog, providing rigorous formal verification. Minlog allows the extraction of executable Haskell programs from proofs, demonstrating their computational utility. The implementations can be found in the folder examples/arith of the Minlog directory. Currently these files are only available and functional in the dev branch of Minlog.
We explore interesting and instructive aspects of the proofs, the implementation in Minlog, and the extracted Haskell term. Additionally, we will highlight the unique features and advantages of Minlog as a proof assistant, offering the audience a deeper insight into its capabilities. The main focus of the presentation will be on the Fundamental Theorem of Arithmetic and Fermat’s factorization method.
-
dc.description.sponsorship
FWF - Österr. Wissenschaftsfonds
-
dc.language.iso
en
-
dc.subject
Minlog
en
dc.subject
Numbertheory
en
dc.subject
Programextraction
en
dc.subject
Fundamental Theorem of Arithmetic
en
dc.subject
Factorisation Methods
en
dc.title
Efficient Program Extraction in Elementary Number Theory using the Proof Assistant Minlog
