Pages that link to "Item:Q2542723"
From MaRDI portal
The following pages link to A proof of cut-elimination theorem in simple type-theory (Q2542723):
Displaying 30 items.
- Kripke semantics for higher-order type theory applied to constraint logic programming languages (Q683712) (← links)
- A simple proof that super-consistency implies cut elimination (Q691121) (← links)
- A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction (Q1075050) (← links)
- A compact representation of proofs (Q1102282) (← links)
- Theory of proofs (arithmetic and analysis) (Q1260035) (← links)
- A semantics for \(\lambda \)Prolog (Q1349686) (← links)
- A cut-free calculus for second-order Gödel logic (Q1677040) (← links)
- Typing and computational properties of lambda expressions (Q1819575) (← links)
- On Takeuti's early view of the concept of set (Q2097059) (← links)
- Mechanized metatheory revisited (Q2323447) (← links)
- Cut-elimination for quantified conditional logic (Q2363418) (← links)
- Vollständigkeit und Schnittelimination in der intuitionistischen Typenlogik (Q2553430) (← links)
- Ein syntaktischer Beweis für die Zulässigkeit der Schnittregel im Kalkül von Schütte für die intuitionistische Typenlogik (Q2558215) (← links)
- Ein starker Normalisationssatz für die intuitionistische Typentheorie (Q2558857) (← links)
- An intensional type theory: motivation and cut-elimination (Q2732287) (← links)
- On the Convergence of Reduction-based and Model-based Methods in Proof Theory (Q2866742) (← links)
- Hauptsatz for higher-order modal logic (Q3043112) (← links)
- Interpolation for first order S5 (Q3149986) (← links)
- A Constructive Semantic Approach to Cut Elimination in Type Theories with Axioms (Q3540178) (← links)
- Annual Meeting of the Association for Symbolic Logic (Q3689157) (← links)
- On nonstandard models in higher order logic (Q3714081) (← links)
- POLYMORPHISM AND THE OBSTINATE CIRCULARITY OF SECOND ORDER LOGIC: A VICTIMS’ TALE (Q4637941) (← links)
- Memories of Kurt Schütte and the logic group in Munich: A personal report (Q5013896) (← links)
- A proof of the cut-elimination theorem in simple type theory (Q5183470) (← links)
- Prawitz, Proofs, and Meaning (Q5213604) (← links)
- Simple type theory of Gentzen style with the inference of extensionality (Q5628098) (← links)
- Resolution in type theory (Q5638281) (← links)
- Neo-Logicism and Its Logic (Q5871286) (← links)
- Completeness of type assignment systems with intersection, union, and type quantifiers (Q5958301) (← links)
- A Survey of the Proof-Theoretic Foundations of Logic Programming (Q6063891) (← links)
