An elementary proof of strong normalization for atomic F

DOI10.18778/0138-0680.45.1.01MaRDI QIDQ2957669zbMATH OpenOpenAlexFDO

Authors Fernando Ferreira, Gilda Ferreira

Publication date 27 January 2017

Published in Bulletin of the Section of Logic (Search for Journal in Brave)

Copyright license Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International

Full work available at URL https://doi.org/10.18778/0138-0680.45.1.01

zbMATH Keywords

elementary proofslambda-calculuspredicative polymorphismstrong normalization

Mathematics Subject Classification ID

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

Recommendations

• Atomic polymorphism
• An elementary proof of strong normalization for intersection types
• scientific article; zbMATH DE number 4134006
• Short Proofs of Strong Normalization
• scientific article; zbMATH DE number 6792338

Cites work

• A simple proof of Parsons' theorem
• An upper bound for reduction sequences in the typed -calculus
• Atomic polymorphism
• Comments on predicative logic
• Constructivism in mathematics. An introduction. Volume I
• Exact bounds for lengths of reductions in typed -calculus
• scientific article; zbMATH DE number 1722646 (Why is no real title available?)
• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 949290 (Why is no real title available?)
• Intensional interpretations of functionals of finite type I
• Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)
• The faithfulness of \(\mathbf{F_{at}}\): a proof-theoretic proof

Cited in

(6)

• Atomic polymorphism and the existence property
• A refined interpretation of intuitionistic logic by means of atomic polymorphism
• scientific article; zbMATH DE number 1722646 (Why is no real title available?)
• -conversions of IPC implemented in atomic F
• The Russell-Prawitz embedding and the atomization of universal instantiation
• The computational content of atomic polymorphism

This page was built for publication: An elementary proof of strong normalization for atomic \(\mathsf F\)

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2957669)