A finite axiomatization of propositional type theory in pure lambda calculus

MaRDI QIDQ3086781zbMATH OpenFDO

Authors Mark Kaminski, Gert Smolka

Publication date 30 March 2011

zbMATH Keywords

propositional type theorysimply typed lambda termspure lambda calculusset-theoretic type hierarchy

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Recommendations

• scientific article; zbMATH DE number 823591
• Some lambda calculus and type theory formalized
• scientific article; zbMATH DE number 2185659
• scientific article; zbMATH DE number 1342246
• scientific article; zbMATH DE number 512879

Cited in

(5)

• Axiomatic rewriting theory II: the   -calculus enjoys finite normalisation cones
• scientific article; zbMATH DE number 3878894 (Why is no real title available?)
• Axioms for the Theory of Lambda-Conversion
• Probabilistic approach to the lambda definability for fourth order types
• Proving properties of typed \(\lambda\)-terms using realizability, covers, and sheaves

Describes a project that uses

Uses Software

• ETPS

This page was built for publication: A finite axiomatization of propositional type theory in pure lambda calculus

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