A note on the proof theory of the \(\lambda \Pi\)-calculus
From MaRDI portal
Publication:1891931
DOI10.1007/BF01063152zbMath0831.03030MaRDI QIDQ1891931
Publication date: 20 February 1996
Published in: Studia Logica (Search for Journal in Brave)
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
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
