Cut elimination in the intuitionistic theory of types with axioms and rewriting cuts, constructively

zbMATH Open1226.03061MaRDI QIDQ3086776FDOQ3086776

James Lipton, Olivier Hermant

Publication date: 30 March 2011

Recommendations

• A Constructive Semantic Approach to Cut Elimination in Type Theories with Axioms
• Completeness and Cut-elimination in the Intuitionistic Theory of Types
• Typed Lambda Calculi and Applications
• Completeness and cut-elimination in the intuitionistic theory of types. II.
• Cut-elimination for simple type theory with an axiom of choice

zbMATH Keywords

cut eliminationconstructive semantic proofintuitionistic formulation of Church's Theory of Types

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05)

Cited In (4)

• Cut-elimination for simple type theory with an axiom of choice
• An intensional type theory: Motivation and cut-elimination
• Cut-Simulation in Impredicative Logics
• Cut Elimination in a Class of Sequent Calculi for Pure Type Systems

This page was built for publication: Cut elimination in the intuitionistic theory of types with axioms and rewriting cuts, constructively

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