Termination of permutative conversions in intuitionistic Gentzen calculi

DOI10.1016/S0304-3975(98)00143-1zbMath0913.68135MaRDI QIDQ1275632

Helmut Schwichtenberg

Publication date: 12 January 1999

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

natural deductionGentzen calculusexplicit substitutionsequentermtermination of permutative conversions

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Characterising Strongly Normalising Intuitionistic Sequent Terms, Variations and interpretations of naturality in call-by-name lambda-calculi with generalized applications, The \(\lambda \)-calculus and the unity of structural proof theory, Permutability of proofs in intuitionistic sequent calculi, A Formalisation of Weak Normalisation (with Respect to Permutations) of Sequent Calculus Proofs

Cites Work

• Permutability of proofs in intuitionistic sequent calculi
• Marginalia on sequent claculi
• The correspondence between cut-elimination and normalization
• Normalization as a homomorphic image of cut-elimination
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item