본문 바로가기
  • Home

A Study on the Relationship Between Hoare Logic and Curry-Howard Correspondence

  • Journal of Knowledge Information Technology and Systems
  • Abbr : JKITS
  • 2020, 15(2), pp.185-193
  • DOI : 10.34163/jkits.2020.15.2.004
  • Publisher : Korea Knowledge Information Technology Society
  • Research Area : Interdisciplinary Studies > Interdisciplinary Research
  • Received : March 22, 2020
  • Accepted : April 10, 2020
  • Published : April 30, 2020

Lee Gye-Sik 1 Hwajeong Kim 2

1한경대학교
2한남대학교

Accredited

ABSTRACT

The relation between computer programs and mathematical logic is well known, Although one can easily find comments on the relationship when one reads books and articles about computer programming, it is difficult to find proper materials explaining the relationship in a scientific manner. Nevertheless, people used to mention how important the relationship between computer programs and mathematical logic is. The problem is that it is more focused on the fact that how helpful it is to learn one area in learning the other area. However, there is more than that between computer programs and mathematical logic. In this paper, we introduce some researches about the relationship and show different and common aspects of them. In particular, Hoare logic and Curry-Howard correspondence is compared. Hoare logic was invented for rigorous verification of programs in a C-like imperative programming language, while Curry-Howard correspondence explains the relationship between functional programming language like Haskell and mathematical logic. We show that Hoare logic and Curry-Howard correspondence are essentially the same in the sense that they represent the same things just in different manners. We close the paper with some remarks about Hoare logic and the Curry-Howard correspondence and ideas of further research with respect to teaching and learning programming languages in the university level based on the relationship between logic and programming.

Citation status

* References for papers published after 2023 are currently being built.