Predicates as types

MaRDI QIDQ5435638zbMATH OpenFDO

Authors Paweł Urzyczyn

Publication date 14 January 2008

zbMATH Keywords

Curry-Howard isomorphismfirst-order arithmeticfirst-order logiclambda calculitutorial

Mathematics Subject Classification ID

Classical first-order logic (03B10) Subsystems of classical logic (including intuitionistic logic) (03B20) Combinatory logic and lambda calculus (03B40) Recursive functions and relations, subrecursive hierarchies (03D20) Cut-elimination and normal-form theorems (03F05) First-order arithmetic and fragments (03F30)

Recommendations

• Lectures on the Curry-Howard isomorphism
• On the adequacy of representing higher order intuitionistic logic as a pure type system
• scientific article; zbMATH DE number 963644
• scientific article; zbMATH DE number 47007
• scientific article; zbMATH DE number 432699

Cited in

(1)

• Inductive data types for predicate transformers

This page was built for publication: Predicates as types

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