Atomic polymorphism

Ferreira, Fernando; Ferreira, Gilda

http://hdl.handle.net/10400.2/9417

Use this identifier to reference this record.

Name:	Description:	Size:	Format:
AtomicPolymorphism.pdf		97.51 KB	Adobe PDF	Download

Send Feedback

Authors

Ferreira, Fernando

Ferreira, Gilda

Abstract(s)

It has been known for six years that the restriction of Girard’s polymorphic system F to atomic universal instantiations interprets the full fragment of the intuitionistic propositional calculus. We firstly observe that Tait’s method of “convertibility” applies quite naturally to the proof of strong normalization of the restricted Girard system. We then show that each β-reduction step of the full intuitionistic propositional calculus translates into one or more βη-reduction steps in the restricted Girard system. As a consequence, we obtain a novel and perspicuous proof of the strong normalization property for the full intuitionistic propositional calculus. It is noticed that this novel proof bestows a crucial role to η-conversions.