Paper Info
Title
A symmetric lambda calculus for classical program extraction
Abstract
In the present paper we introduce a -calculus with symmetric reduction rules and classical types, i.e. types corresponding to formulas of classical propositional logic. Strong normalization property is proved to hold for such a calculus. We then extend this calculus in order to get a system equivalent to Peano Arithmetic and show, by means of a theorem on the shape of terms in normal form, how to get recursive functions out of proofs of 2 0 formulas, i.e. the ones corresponding to program specifications.
Year
DOI
Venue
1994
10.1006/inco.1996.0025
Information and Computation - special issue: symposium on theoretical aspects of computer software TACS '94
Keywords
DocType
Volume
symmetric lambda calculus,program extraction,classical program extraction,lambda calculus,propositional logic,normal form,peano arithmetic
Conference
125
Issue
ISSN
Citations 
2
0890-5401
46
PageRank 
References 
Authors
3.48
5
2
Name
Order
Citations
PageRank
Franco Barbanera135735.14
Stefano Berardi237351.58