@article{ART002581761},

author={Lee Gye-Sik and Hwajeong Kim},

title={A Study on the Relationship Between Hoare Logic and Curry-Howard Correspondence},

journal={Journal of Knowledge Information Technology and Systems},

issn={1975-7700},

year={2020},

volume={15},

number={2},

pages={185-193},

doi={10.34163/jkits.2020.15.2.004}

TY - JOUR

AU - Lee Gye-Sik

AU - Hwajeong Kim

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

JO - Journal of Knowledge Information Technology and Systems

PY - 2020

VL - 15

IS - 2

PB - Korea Knowledge Information Technology Society

SP - 185

EP - 193

SN - 1975-7700

AB - 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.

KW - Hoare logic;Curry-Howard correspondence;Correctness proof;Mathematical logic;Lambda calculus

DO - 10.34163/jkits.2020.15.2.004

ER -

Lee Gye-Sik and Hwajeong Kim. (2020). A Study on the Relationship Between Hoare Logic and Curry-Howard Correspondence. Journal of Knowledge Information Technology and Systems, 15(2), 185-193.

Lee Gye-Sik and Hwajeong Kim. 2020, "A Study on the Relationship Between Hoare Logic and Curry-Howard Correspondence", Journal of Knowledge Information Technology and Systems, vol.15, no.2 pp.185-193. Available from: doi:10.34163/jkits.2020.15.2.004

Lee Gye-Sik, Hwajeong Kim "A Study on the Relationship Between Hoare Logic and Curry-Howard Correspondence" Journal of Knowledge Information Technology and Systems 15.2 pp.185-193 (2020) : 185.

Lee Gye-Sik, Hwajeong Kim. A Study on the Relationship Between Hoare Logic and Curry-Howard Correspondence. 2020; 15(2), 185-193. Available from: doi:10.34163/jkits.2020.15.2.004

Lee Gye-Sik and Hwajeong Kim. "A Study on the Relationship Between Hoare Logic and Curry-Howard Correspondence" Journal of Knowledge Information Technology and Systems 15, no.2 (2020) : 185-193.doi: 10.34163/jkits.2020.15.2.004

Lee Gye-Sik; Hwajeong Kim. A Study on the Relationship Between Hoare Logic and Curry-Howard Correspondence. Journal of Knowledge Information Technology and Systems, 15(2), 185-193. doi: 10.34163/jkits.2020.15.2.004

Lee Gye-Sik; Hwajeong Kim. A Study on the Relationship Between Hoare Logic and Curry-Howard Correspondence. Journal of Knowledge Information Technology and Systems. 2020; 15(2) 185-193. doi: 10.34163/jkits.2020.15.2.004

Lee Gye-Sik, Hwajeong Kim. A Study on the Relationship Between Hoare Logic and Curry-Howard Correspondence. 2020; 15(2), 185-193. Available from: doi:10.34163/jkits.2020.15.2.004

Lee Gye-Sik and Hwajeong Kim. "A Study on the Relationship Between Hoare Logic and Curry-Howard Correspondence" Journal of Knowledge Information Technology and Systems 15, no.2 (2020) : 185-193.doi: 10.34163/jkits.2020.15.2.004