A note on the proof theory of the \(\lambda \Pi\)-calculus

DOI10.1007/BF01063152zbMath0831.03030MaRDI QIDQ1891931

David J. Pym

Publication date: 20 February 1996

Published in: Studia Logica (Search for Journal in Brave)

zbMATH Keywords

sequent calculusnatural deductioncut-eliminationproof searchLogical Framework

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Cut-elimination and normal-form theorems (03F05)

Related Items

On the intuitionistic force of classical search (Extended abstract) ⋮ On the intuitionistic force of classical search

Uses Software

• Elf

Cites Work

• Using typed lambda calculus to implement formal systems on a machine
• Gentzenizing Schroeder-Heister's natural extension of natural deduction
• Generalized algebraic theories and contextual categories
• Untersuchungen über das logische Schliessen. I
• Uniform proofs as a foundation for logic programming
• Herbrand analyses
• A natural extension of natural deduction
• A framework for defining logics
• The correspondence between cut-elimination and normalization
• What is a model of the lambda calculus?
• Introduction to generalized type systems
• A UNIFICATION ALGORITHM FOR THE λΠ-CALCULUS
• A Machine-Oriented Logic Based on the Resolution Principle
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item