Iranian Association of Logic
Owner
Iranian Association of Logic (IAL) is the owner of Logical Letter.
Volume 1, Issue 1 (2026)
3 2026, 1(1): 22-28 |
Back to browse issues page
Request Type: Original Research |
Received: 2026/10/21 | Accepted: 2027/01/2 | Published: 2027/01/2
Received: 2026/10/21 | Accepted: 2027/01/2 | Published: 2027/01/2
Download citation:
BibTeX | RIS | EndNote | Medlars | ProCite | Reference Manager | RefWorks
Send citation to:
BibTeX | RIS | EndNote | Medlars | ProCite | Reference Manager | RefWorks
Send citation to:
Mirsanei A. Logic Meets Computation: From the Curry--Howard Correspondence to Proof Assistants. 3 2026; 1 (1) :22-28
URL: http://daneshafarand.org/article-9-87270-en.html
URL: http://daneshafarand.org/article-9-87270-en.html
Tarbiat Modares University
Abstract: (1 Views)
Aims This article explains the correspondence between proofs and programs known as the Curry--Howard correspondence, and shows how it has led to proof assistants that are now used to verify both mathematics and software.
Approach Starting from natural deduction and the simply typed lambda calculus, the article sets out the correspondence between propositions and types, proofs and programs, and proof normalization and evaluation, follows its main extensions, and reviews the leading proof assistants and their applications.
Main Points The correspondence is not an analogy but a precise structural identity: a proof in intuitionistic natural deduction is a typed program, and simplifying the proof is running the program. Dependent types extend the correspondence to quantifiers and allow mathematical statements and their proofs to be written and checked in a single language.
Conclusion The correspondence has turned an abstract result of logic into a practical technology that has verified major theorems and critical software.
Approach Starting from natural deduction and the simply typed lambda calculus, the article sets out the correspondence between propositions and types, proofs and programs, and proof normalization and evaluation, follows its main extensions, and reviews the leading proof assistants and their applications.
Main Points The correspondence is not an analogy but a precise structural identity: a proof in intuitionistic natural deduction is a typed program, and simplifying the proof is running the program. Dependent types extend the correspondence to quantifiers and allow mathematical statements and their proofs to be written and checked in a single language.
Conclusion The correspondence has turned an abstract result of logic into a practical technology that has verified major theorems and critical software.
Keywords: Curry--Howard Correspondence, Lambda Calculus, Type Theory, Proof Assistants, Formal Verification
| Rights and permissions | |
 |
This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License. |