Direkt zum Inhalt

One Monad to Prove Them All

Abstract

One Monad to Prove Them All is a modern fairy tale about curiosity and perseverance, two important properties of a successful PhD student. We follow the PhD student Mona on her adventure of proving properties about Haskell programs in the proof assistant Coq. On the one hand, as a PhD student in computer science Mona observes an increasing demand for correct software products. In particular, because of the large amount of existing software, verifying existing software products becomes more important. Verifying programs in the functional programming language Haskell is no exception. On the other hand, Mona is delighted to see that communities in the area of theorem proving are becoming popular. Thus, Mona sets out to learn more about the interactive theorem prover Coq and verifying Haskell programs in Coq.

Zitieren

Dylus S, Christiansen J, Teegen F. One Monad to Prove Them All. The Art, Science, and Engineering of Programming. 2019;3. doi:10.22152/programming-journal.org/2019/3/8.
Dylus, S., Christiansen, J., & Teegen, F. (2019). One Monad to Prove Them All. The Art, Science, And Engineering Of Programming, 3. http://doi.org/10.22152/programming-journal.org/2019/3/8
Dylus, Sandra, Jan Christiansen, und Finn Teegen. 2019. „One Monad To Prove Them All“. The Art, Science, And Engineering Of Programming 3. doi:10.22152/programming-journal.org/2019/3/8.
Dylus, Sandra, Jan Christiansen, und Finn Teegen. „One Monad To Prove Them All“. The Art, Science, and Engineering of Programming 3 (2019): n. pag.
Dylus, S., u. a. „One Monad To Prove Them All“. The Art, Science, And Engineering Of Programming, 3, 2019.

Details

  • Volume

    3
  • ISSN Number

    2473-7321