Title: Classical logic, storage operators and second-order lambda-calculus
Abstract: We describe here a simple method in order to obtain programs from proofs in second-order classical logic. Then we extend to classical logic the results about storage operators (typed λ-terms which simulate call-by-value in call-by-name) proved by Krivine (1990) for intuitionistic logic. This work generalizes previous results of Parigot (1992).
Publication Year: 1994
Publication Date: 1994-06-01
Language: en
Type: article
Indexed In: ['crossref']
Access and Citation
Cited By Count: 78
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot