Opis

• Title:
  An Elementary Proof of Strong Normalization for Atomic F
• Creator:
  Ferreira, Fernando;
  Ferreira, Gilda
• Contributor:
  Universidade de Lisboa;
  Universidade Lus´ofona de Humanidades e Tecnologias;
  gmferreira@fc.ul.pt
• Description:
  2010 Mathematics Subject Classification. 03F07, 03B20, 03B40;
  We give an elementary proof (in the sense that it is formalizable in Peano arithmetic) of the strong normalization of the atomic polymorphic calculus F_{at} (a predicative restriction of Girard’s system F).;
  Both authors acknowledge the support of Fundação para a Ciência e a Tecnologia [UID/MAT/04561/2013] and Centro de Matemática, Aplicações Fundamentais e Investigação Operacional of Universidade de Lisboa. The second author is also grateful to Fundação para a Ciência e a Tecnologia [UID/CEC/00408/2013 and grant SFRH/BPD/93278/2013], to LargeScale Informatics Systems Laboratory (Universidade de Lisboa) and to Núcleo de Investigação em Matemática (Universidade Lusófona).
• Object availability:
  Dostęp otwarty
• Date:
  2016.12.08;
  2016
• Type:
  Article
• Language:
  angielski
• Format:
  application/pdf
• Publisher:
  Uniwersytet Łódzki. Katedra Logiki i Metodologii Nauk
• Relation:
  Uniwersytet Łódzki. Katedra Logiki i Metodologii Nauk;45;
  1
• Subject:
  predicative polymorphism;
  strong normalization;
  elementary proofs;
  lambda-calculus
• Identifier:
  0138-0680;
  http://hdl.handle.net/11089/20145 ;
  2449-836X;
  10.18778/0138-0680.45.1.01
• Data provider:
  Repozytorium Uniwersytetu Łódzkiego
• Can I use it?:
  poproś o pozwolenie
• Type:
  obrazy