scientific article; zbMATH DE number 4099299

MaRDI QIDQ3824315zbMATH OpenFDO

Authors Pierre Ageron

Publication date 1988

Full work available at URL https://eudml.org/doc/193018

zbMATH Keywords

algebraic theory of typesGirard's system F of second order lambda-calculuslogical theory of typestype in a category

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Second- and higher-order arithmetic and fragments (03F35) Categorical logic, topoi (03G30) Equational categories (18C05)

Recommendations

• scientific article; zbMATH DE number 4152661
• scientific article; zbMATH DE number 176139
• scientific article; zbMATH DE number 92598
• scientific article; zbMATH DE number 4099537
• Comprehension categories and the semantics of type dependency
• A general semantic construction of dependent refinement type systems, categorically
• \(F\)-semantics for type assignment systems
• scientific article; zbMATH DE number 4074446
• Towards formalizing categorical models of type theory in type theory

Cited in

(6)

• The system \({\mathcal F}\) of variable types, fifteen years later
• A quantitative interpretation of Girard's System F
• scientific article; zbMATH DE number 4152661 (Why is no real title available?)
• scientific article; zbMATH DE number 4021135 (Why is no real title available?)
• scientific article; zbMATH DE number 4099537 (Why is no real title available?)
• Proof-oriented categorical semantics

This page was built for publication:

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