Non-strictly positive fixed points for classical natural deduction

DOI10.1016/j.apal.2004.10.009zbMath1066.03057OpenAlexW1971181861MaRDI QIDQ1772778

Ralph Matthes

Publication date: 21 April 2005

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.apal.2004.10.009

zbMATH Keywords

strong normalizationfixed point operatorclassical \(\lambda\mu\)-calculus

Mathematics Subject Classification ID

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

Related Items (8)

A semantical proof of the strong normalization theorem for full propositional classical natural deduction ⋮ Strong normalization proofs by CPS-translations ⋮ Some properties of the -calculus ⋮ Strong normalization results by translation ⋮ Inhabitation of polymorphic and existential types ⋮ Strong normalization of classical natural deduction with disjunctions ⋮ Two extensions of system F with (co)iteration and primitive (co)recursion principles ⋮ A simple proof of second-order strong normalization with permutative conversions

Cites Work

• A semantical proof of the strong normalization theorem for full propositional classical natural deduction
• Perpetual reductions in \(\lambda\)-calculus
• Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)
• On the intuitionistic force of classical search
• Church-Rosser property of a simple reduction for full first-order classical natural deduction
• Type fixpoints
• Normalization theorems for full first order classical natural deduction
• Un plongement de la logique classique du 2nd ordre dans AF2
• Proofs of strong normalisation for second order classical natural deduction
• A short proof of the strong normalization of classical natural deduction with disjunction
• Parallel reductions in \(\lambda\)-calculus
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Non-strictly positive fixed points for classical natural deduction