Completeness and Cut-elimination in the Intuitionistic Theory of Types

DOI10.1093/LOGCOM/EXI055zbMath1095.03056OpenAlexW1969802940MaRDI QIDQ3371147

James Lipton, Mary Demarco

Publication date: 21 February 2006

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

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

zbMATH Keywords

theorem provingproof theorycut-eliminationlogic programminglambda calculustype theoryimpredicative formal systems

Mathematics Subject Classification ID

Logic in computer science (03B70) Mechanization of proofs and logical operations (03B35) Cut-elimination and normal-form theorems (03F05) Logic programming (68N17) Combinatory logic and lambda calculus (03B40)

Related Items (7)

Reconsidering pairs and functions as sets ⋮ First-order automated reasoning with theories: when deduction modulo theory meets practice ⋮ A Constructive Semantic Approach to Cut Elimination in Type Theories with Axioms ⋮ Kripke semantics for higher-order type theory applied to constraint logic programming languages ⋮ A simple proof that super-consistency implies cut elimination ⋮ Abstract deduction and inferential models for type theory ⋮ On the Convergence of Reduction-based and Model-based Methods in Proof Theory

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