Atomic polymorphism

DOI10.2178/jsl.7801180zbMath1279.03035OpenAlexW4214703049MaRDI QIDQ4916559

Gilda Ferreira, Fernando Ferreira

Publication date: 23 April 2013

Published in: The Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: https://projecteuclid.org/euclid.jsl/1358951113

zbMATH Keywords

natural deductionstrong normalizationpredicative polymorphismsecond-order \(\lambda \)-calculus

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Combinatory logic and lambda calculus (03B40)

Related Items (8)

Rasiowa-Harrop disjunction property ⋮ The naturality of natural deduction ⋮ A refined interpretation of intuitionistic logic by means of atomic polymorphism ⋮ Elementary Proof of Strong Normalization for Atomic F ⋮ The faithfulness of \(\mathbf{F_{at}}\): a proof-theoretic proof ⋮ Unnamed Item ⋮ Atomic polymorphism and the existence property ⋮ The naturality of natural deduction. II: on atomic polymorphism and generalized propositional connectives

Cites Work

• Unnamed Item
• Unnamed Item
• Parameter-free polymorphic types
• Commuting conversions vs. the standard conversions of the ``good connectives
• Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)
• Comments on predicative logic

This page was built for publication: Atomic polymorphism