Completeness and Cut-elimination in the Intuitionistic Theory of Types--Part 2

DOI10.1093/logcom/exp076zbMath1188.03042OpenAlexW4238160626MaRDI QIDQ3553922

Olivier Hermant, James Lipton

Publication date: 21 April 2010

Published in: Journal of Logic and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1093/logcom/exp076

zbMATH Keywords

tableauxcut eliminationsequent calculusintuitionistic theory of types

Mathematics Subject Classification ID

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

Related Items (1)

A simple proof that super-consistency implies cut elimination

This page was built for publication: Completeness and Cut-elimination in the Intuitionistic Theory of Types--Part 2