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

DOI10.1007/3-540-45013-0_2MaRDI QIDQ3079922zbMATHOpenAlexFDO

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

sequent calculicut eliminationpure type systemslambda calculus with types

Mathematics Subject Classification ID

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

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
• Cut Elimination in a Class of Sequent Calculi for Pure Type Systems
• scientific article; zbMATH DE number 2038767 (Why is no real title available?)
• A Sequent Calculus for Type Theory

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)