scientific article; zbMATH DE number 2185711

MaRDI QIDQ3024903zbMATH OpenFDO

Authors Judicaël Courant

Publication date 4 July 2005

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40)

Recommendations

• A module calculus for Pure Type Systems
• Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo
• scientific article; zbMATH DE number 1499107
• A modular construction of type theories
• Theory of types and decision procedures

Cited in

(11)

• Dependent types with subtyping and late-bound overloading
• Types for modules
• Types for the ambient calculus
• A type system for higher-order modules
• A module calculus for Pure Type Systems
• Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo
• A Modular Type Reconstruction Algorithm
• Automath and Pure Type Systems
• Modeling abstract types in modules with open existential types
• Types for Proofs and Programs
• Principal Type Schemes for Modular Programs

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 Q3024903)