A cut-free sequent calculus for pure type systems verifying the structural rules of Gentzen/Kleene

DOI10.1007/3-540-45013-0_2MaRDI QIDQ3079922zbMATH OpenOpenAlexFDO

Authors

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 eliminationlambda calculus with typespure type systemssequent calculi

Mathematics Subject Classification ID

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

Recommendations

• Cut Elimination in a Class of Sequent Calculi for Pure Type Systems
• scientific article; zbMATH DE number 2038767
• A Sequent Calculus for Type Theory
• A focused sequent calculus framework for proof search in pure type systems
• Structural cut elimination. I: Intuitionistic and classical logic

Cited in

(4)

• A Cut-Free and Invariant-Free Sequent Calculus for PLTL
• A Sequent Calculus for Type Theory
• scientific article; zbMATH DE number 2038767 (Why is no real title available?)
• Cut Elimination in a Class of Sequent Calculi for Pure Type Systems

Describes a project that uses

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3079922)