Atomic polymorphism

Registro completo de metadados
MetadadosDescriçãoIdioma
Autor(es): dc.creatorFerreira, Fernando-
Autor(es): dc.creatorFerreira, Gilda-
Data de aceite: dc.date.accessioned2020-09-24T17:26:28Z-
Data de disponibilização: dc.date.available2020-09-24T17:26:28Z-
Data de envio: dc.date.issued2020-03-02-
Data de envio: dc.date.issued2020-03-02-
Data de envio: dc.date.issued2013-
Fonte completa do material: dc.identifierhttp://hdl.handle.net/10400.2/9417-
Fonte: dc.identifier.urihttp://educapes.capes.gov.br/handle/10400.2/9417-
Descrição: dc.descriptionIt 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.-
Descrição: dc.descriptionBoth authors acknowledge support of FCT-Fundação para a Ciência e a Tecnologia [project PTDC/MAT/104716/2008] and Centro de Matematica e Aplicações Fundamentais (Universidade de Lisboa). The second author is also grateful to FCT [grant SFRH/BPD/34527/2006] and Nucleo de Investigação em Matemática (Universidade Lusófona).-
Descrição: dc.descriptioninfo:eu-repo/semantics/publishedVersion-
Idioma: dc.languageen-
Publicador: dc.publisherThe Journal of Symbolic Logic-
Relação: dc.relationinfo:eu-repo/grantAgreement/FCT/3599-PPCDT/104716/PT-
Relação: dc.relationinfo:eu-repo/grantAgreement/FCT/SFRH/SFRH%2FBPD%2F34527%2F2006/PT-
Direitos: dc.rightsopenAccess-
Palavras-chave: dc.subjectPredicative polymorphism-
Palavras-chave: dc.subjectStrong normalization-
Palavras-chave: dc.subjectNatural deduction-
Palavras-chave: dc.subjectSecond order lambda-calculus-
Palavras-chave: dc.subjectODS::04:Educação de Qualidade-
Título: dc.titleAtomic polymorphism-
Tipo de arquivo: dc.typelivro digital-
Aparece nas coleções:Repositório Aberto - Universidade Aberta (Portugal)

Não existem arquivos associados a este item.