This is a really cool paper. That correspondence is really something!
Paper review: Proofs are Programs This paper is written in a quite readable and interesting way. Using a few symbols and detailed narration, it draws out a picture to illustrate essences of natural deduction and lambda calculus and their correspondences. And now these principles are bases and guides for designing programming languages and especially type system in these languages. The conclusion of the paper gives extensive examples how programming languages exploiting the principles in different way. Thus, the paper is a good introductory paper for us to explore more in direction of refining and designing theorem provers, solving code security problem and so on, though there is no much new idea in this paper. After reading this paper, I knew the evolution of Gentzen¡¯s natural deduction and the lambda calculus and typed lambda calculus more clearly. So understanding why proofs are programs is easier. It is interesting to see how computing universe can be built from just three term forms and one reduction rule. The merit of this paper are summarizing them out, explaining then clearly and showing examples. Hm.. I do not see anything redundant in this paper as a narration paper.
This paper set out to show (as the title implies) how proofs and programs can be viewed as the same thing. To this end, the paper does a resonablly good job. However, it would have been nice to see the case made a little more concrete. The two major points made in support of this argument seem to be the extreme flexability of lambda calculus and the ability to use formal proofs for type checking. Certainly these ideas do take us a long way, but perhaps I was looking for a cleaner, 1 to 1 mapping between the two paradigms. In retrospect, this likely isn't achievable. And, if it is, it would take much more discussion than the 15 pages of this paper. Having said that, I really enjoyed reading this paper. For me, it did so much more than just explain how proofs are programs. The historial background on lambda calculus and type systems was very well written and provided a lot of insight into the conveluted notation that we use today. In addition, the discussion of typed lambda calculus took a topic that is full of complex notation and described it in a clean and precise maner. Perhaps this paper should be made mandatory for systems folk like myself (i.e., those who last touched lambda calculus over 7 years ago). While the historical background about lamba calculus was certainly interesting, my favorite part of this paper was the conclusion. As someone who works in the field of security research, I took great interest in seeing the connections being drawn between typed langugages and security. Specifically, the discussion on proof carrying code presented some interesting research areas of great importance to a person like me. Overall, I felt that the paper was well written and presented the material in a very approachable fashion.
This paper can be an introductory reading for fields such as lambda calculus, logic, type systems or computational models. Written in an "easy-digestable" way, it starts with an introduction of formal logic and lambda calculus, augmented with historical facts. After that, the author presents typed lambda-calculus as a small introduction to type-systems, and refers to the correspondence of lambda calculus and Gentzen's logic system. Enriched with many historical (but still interesting) references, the paper presents the still-ongoing correspondance between mathematical logic and computation models/programming languages. Concluding, there is a wide reference to (functional) programming languages, since their beginning with lisp. Most past and current functional languages are mentioned, and the fact that many successful theorem provers are written in functional languages is stressed (correspondance). The issue of safety and type-checking as a safety tool is discussed towards the end of the paper, and proposed solutions for safety are presented. This is the only part of the paper that non-functional languages are mentioned (Java, C, C++, Modula-3, TAL, etc), to stress the fact that even non-fuctional languages' typesystems correspond to theorem-proofs in mathematical logic. Overall, it is a well-written paper, that presents in an intuitive way the correspondence between formal proofs and computer programs/typesystems. It succeeds in inciting the reader's curiosity on the type-systems' field, and contains many references, both historical and current, mathematical and application-oriented. The only thing missing is a formal list of references in the end, that would forward the reader to more technical/formal readings, although they are referenced in the text.
This paper gives the realtionship between the logic and the stored program computer.This paper explains the Gentzen's natural deduction and Church's lambda calculus.In the early part of the paper author describes the theory behid the Gentzen's natural deduction and church's lambda Calculus.The Gentzen's natural system has structural and logical rules.This paper also highlights the subforula property of the Gentzen's paper.Gentzen presents the various ways of formatting logic,natural deduction and sequent calculus. Church's lambda brings the concep of the typed systems.Functional programing and types are used used in almost all the languages. In the later section of the paper the auther explians the concept of Theorem provers and Proof Carrying Code.Types ensure the security.According to the paper the types are checked before running which is economical.There is a desciption of the difference of the type checkers of Java and TAL. In the end of the paper PCC 's advantageas and disadvantages are mentioned.Unlike TAL ,instead of adding types to the machine code one adds the proof directly.Example of PCC are packet filters Java. so in short Proofs are Programs.
The heart of this paper is the Curry-Howard correspondance, and it presents this in a clear manner, with good historical background and examples. Papers such as this one, which do not contribute new results, but instead frame and link together past research, must obviously be evaluated by different criteria than articles on new or ongoing research. Clarity and interest are perhaps two of the primary criteria. On the first I have no complaints; the color used in the type derivation aids comprehension, and the gradual development is easy to follow, yet still surprising when the fundamental result is revealed. Correspondences like this are almost always of interest, as they help to distill ideas down to their essences. Understanding that proofs and programs are the same helps us to understand what they really do. The primary thing that I think could improve this paper is a list of references. The conclusions section lists many interesting consequences and related work, but doesn't tell you where to go to find more about it. I assume this was done because each subject mentioned spans many papers and giving just one would not be representative.
Generated: Thu Mar 6 15:39:24 EST 2003 by mwh