dc.contributor.author | Kiiskinen, Sampsa | |
dc.contributor.editor | Neittaanmäki, Pekka | |
dc.contributor.editor | Rantalainen, Marja-Leena | |
dc.date.accessioned | 2024-01-09T09:10:36Z | |
dc.date.available | 2024-01-09T09:10:36Z | |
dc.date.issued | 2023 | |
dc.identifier.citation | Kiiskinen, S. (2023). Curiously Empty Intersection of Proof Engineering and Computational Sciences. In P. Neittaanmäki, & M.-L. Rantalainen (Eds.), <i>Impact of Scientific Computing on Science and Society</i> (pp. 45-73). Springer. Computational Methods in Applied Sciences, 58. <a href="https://doi.org/10.1007/978-3-031-29082-4_3" target="_blank">https://doi.org/10.1007/978-3-031-29082-4_3</a> | |
dc.identifier.other | CONVID_183921931 | |
dc.identifier.uri | https://jyx.jyu.fi/handle/123456789/92598 | |
dc.description.abstract | The tools and techniques of proof engineering have not yet been applied to the computational sciences. We try to explain why and investigate their potential to advance the field. More concretely, we formalize elementary group theory in an interactive theorem prover and discuss how the same technique could be applied to formalize general computational methods, such as discrete exterior calculus. We note that such formalizations could reveal interesting insights into the mathematical structure of the methods and help us implement them with stronger guarantees of correctness. We also postulate that working in this way could dramatically change the way we study and communicate computational sciences. | en |
dc.format.extent | 450 | |
dc.format.mimetype | application/pdf | |
dc.language.iso | eng | |
dc.publisher | Springer | |
dc.relation.ispartof | Impact of Scientific Computing on Science and Society | |
dc.relation.ispartofseries | Computational Methods in Applied Sciences | |
dc.rights | In Copyright | |
dc.subject.other | proof engineering | |
dc.subject.other | type theory | |
dc.subject.other | software engineering | |
dc.subject.other | formal verification | |
dc.subject.other | interactive theorem provers | |
dc.subject.other | abstract algebra | |
dc.subject.other | functional programming | |
dc.title | Curiously Empty Intersection of Proof Engineering and Computational Sciences | |
dc.type | bookPart | |
dc.identifier.urn | URN:NBN:fi:jyu-202401091100 | |
dc.contributor.laitos | Informaatioteknologian tiedekunta | fi |
dc.contributor.laitos | Faculty of Information Technology | en |
dc.contributor.oppiaine | Computing, Information Technology and Mathematics | fi |
dc.contributor.oppiaine | Laskennallinen tiede | fi |
dc.contributor.oppiaine | Computing, Information Technology and Mathematics | en |
dc.contributor.oppiaine | Computational Science | en |
dc.type.uri | http://purl.org/eprint/type/BookItem | |
dc.relation.isbn | 978-3-031-29081-7 | |
dc.type.coar | http://purl.org/coar/resource_type/c_3248 | |
dc.description.reviewstatus | peerReviewed | |
dc.format.pagerange | 45-73 | |
dc.relation.issn | 1871-3033 | |
dc.type.version | acceptedVersion | |
dc.rights.copyright | © 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG | |
dc.rights.accesslevel | openAccess | fi |
dc.subject.yso | ohjelmistotuotanto | |
dc.subject.yso | verifiointi | |
dc.subject.yso | ohjelmointi | |
dc.format.content | fulltext | |
jyx.subject.uri | http://www.yso.fi/onto/yso/p17097 | |
jyx.subject.uri | http://www.yso.fi/onto/yso/p6609 | |
jyx.subject.uri | http://www.yso.fi/onto/yso/p4887 | |
dc.rights.url | http://rightsstatements.org/page/InC/1.0/?language=en | |
dc.relation.doi | 10.1007/978-3-031-29082-4_3 | |
dc.type.okm | A3 | |