Description

• Title:
  Elementary Proof of Strong Normalization for Atomic F
• Creator:
  Ferreira, Fernando;
  Ferreira, Gilda
• Contributor:
  Universidade de Lisboa, Faculdade de Ciências, Departamento de Matemática;
  Universidade Lusófona de Humanidades e Tecnologias, Departamento de Matemática;
  fjferreira@fc.ul.pt;
  gmferreira@fc.ul.pt
• Description:
  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ₐₜ (a predicative restriction of Girard’s system F).
• Object availability:
  free access
• Rights:
  © Copyright by Authors, Łódź 2016; © Copyright for this edition by Uniwersytet Łódzki, Łódź 2016
• Date:
  2017.05.16;
  2016
• Type:
  Article
• Language:
  English
• Format:
  application/pdf
• Publisher:
  Wydawnictwo Uniwersytetu Łódzkiego
• Relation:
  Bulletin of the Section of Logic;1;
  45
• Subject:
  Predicative polymorphism;
  strong normalization;
  elementary proofs;
  lambda-calculus
• Identifier:
  0138-0680;
  http://hdl.handle.net/11089/21620 ;
  2449-836X;
  10.18778/0138-0680.45.1.01
• Data provider:
  Repozytorium Uniwersytetu Łódzkiego
• Can I use it?:
  seek permission
• Type:
  image