A Cut-Free Sequent Calculus for Pure Type Systems Verifying the Structural Rules of Gentzen/Kleene

DOI10.1007/3-540-45013-0_2zbMath1278.03037OpenAlexW1521303708MaRDI QIDQ3079922

No author found.

Publication date: 4 March 2011

Published in: Logic Based Program Synthesis and Transformation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-45013-0_2

zbMATH Keywords

cut eliminationpure type systemssequent calculilambda calculus with types

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Combinatory logic and lambda calculus (03B40)

Related Items (1)

Cut Elimination in a Class of Sequent Calculi for Pure Type Systems

Uses Software

• Automath

This page was built for publication: A Cut-Free Sequent Calculus for Pure Type Systems Verifying the Structural Rules of Gentzen/Kleene