Atenção: Todas as denúncias são sigilosas e sua identidade será preservada.
Os campos nome e e-mail são de preenchimento opcional
Metadados | Descrição | Idioma |
---|---|---|
Autor(es): dc.creator | Ferreira, Fernando | - |
Autor(es): dc.creator | Ferreira, Gilda | - |
Data de aceite: dc.date.accessioned | 2020-09-24T17:26:28Z | - |
Data de disponibilização: dc.date.available | 2020-09-24T17:26:28Z | - |
Data de envio: dc.date.issued | 2020-03-02 | - |
Data de envio: dc.date.issued | 2020-03-02 | - |
Data de envio: dc.date.issued | 2013 | - |
Fonte completa do material: dc.identifier | http://hdl.handle.net/10400.2/9417 | - |
Fonte: dc.identifier.uri | http://educapes.capes.gov.br/handle/10400.2/9417 | - |
Descrição: dc.description | 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. | - |
Descrição: dc.description | Both 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.description | info:eu-repo/semantics/publishedVersion | - |
Idioma: dc.language | en | - |
Publicador: dc.publisher | The Journal of Symbolic Logic | - |
Relação: dc.relation | info:eu-repo/grantAgreement/FCT/3599-PPCDT/104716/PT | - |
Relação: dc.relation | info:eu-repo/grantAgreement/FCT/SFRH/SFRH%2FBPD%2F34527%2F2006/PT | - |
Direitos: dc.rights | openAccess | - |
Palavras-chave: dc.subject | Predicative polymorphism | - |
Palavras-chave: dc.subject | Strong normalization | - |
Palavras-chave: dc.subject | Natural deduction | - |
Palavras-chave: dc.subject | Second order lambda-calculus | - |
Palavras-chave: dc.subject | ODS::04:Educação de Qualidade | - |
Título: dc.title | Atomic polymorphism | - |
Tipo de arquivo: dc.type | livro digital | - |
Aparece nas coleções: | Repositório Aberto - Universidade Aberta (Portugal) |
O Portal eduCAPES é oferecido ao usuário, condicionado à aceitação dos termos, condições e avisos contidos aqui e sem modificações. A CAPES poderá modificar o conteúdo ou formato deste site ou acabar com a sua operação ou suas ferramentas a seu critério único e sem aviso prévio. Ao acessar este portal, você, usuário pessoa física ou jurídica, se declara compreender e aceitar as condições aqui estabelecidas, da seguinte forma: