KJCKorea
Journal Central

@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