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

DOI10.1007/3-540-45013-0_2zbMATH Open1278.03037OpenAlexW1521303708MaRDI QIDQ3079922FDOQ3079922

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

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

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)

Cited In (4)

• Title not available (Why is that?)
• A Sequent Calculus for Type Theory
• A Cut-Free and Invariant-Free Sequent Calculus for PLTL
• 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

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