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

MaRDI QIDQ3086776zbMATH OpenFDO

Authors Olivier Hermant, James Lipton

Publication date 30 March 2011

zbMATH Keywords

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

Mathematics Subject Classification ID

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

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

Cited in

(9)

• Cut-Simulation and Impredicativity
• Cut-elimination for simple type theory with an axiom of choice
• An intensional type theory: Motivation and cut-elimination
• Completeness and cut-elimination in the intuitionistic theory of types. II.
• Cut-Simulation in Impredicative Logics
• Cut Elimination in a Class of Sequent Calculi for Pure Type Systems
• A Constructive Semantic Approach to Cut Elimination in Type Theories with Axioms
• Quick cut-elimination for strictly positive cuts
• Completeness and Cut-elimination in the Intuitionistic Theory of Types

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)