논문윤리하기 논문투고규정
  • 오늘 가입자수 0
  • 오늘 방문자수 200
  • 어제 방문자수 435
  • 총 방문자수 2790
2024-11-01 08:20am
논문지
HOME 자료실 > 논문지

발간년도 : [2020]

 
논문정보
논문명(한글) [Vol.15, No.2] A Study on the Relationship between Hoare Logic and Curry-Howard Correspondence
논문투고자 Gyesik Lee, Hwajeong Kim
논문내용 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.
첨부논문
   15-2-04.pdf (894.5K) [4] DATE : 2020-05-07 11:33:01