Elementary proof of strong normalization for Atomic F

We give an elementary proof (in the sense that it is formalizable in Peano arithmetic) of the strong normalization of the atomic polymorphic calculus Fat (a predicative restriction of Girard’s system F).

Bibliographic Details
Main Author: Ferreira, Fernando (author)
Other Authors: Ferreira, Gilda (author)
Format: article
Language:eng
Published: 2021
Subjects:
Predicative polymorphism
Strong normalization
Elementary proofs
Lambda-calculus
Online Access:http://hdl.handle.net/10400.2/10492
Country:Portugal
Oai:oai:repositorioaberto.uab.pt:10400.2/10492

Internet

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

Similar Items