On the expressive power of schemes

DOI10.1016/j.ic.2011.06.003zbMath1241.03070OpenAlexW2080915657MaRDI QIDQ719245

Gilles Dowek, Ying Jiang

Publication date: 10 October 2011

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2011.06.003

zbMATH Keywords

natural deductionbound variableproof normalization

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07) Combinatory logic and lambda calculus (03B40)

Related Items (1)

Unnamed Item

Cites Work

• Mechanical procedure for proof construction via closed terms in typed \(\lambda\) calculus
• Theorem proving modulo
• Normal proofs and their grammar
• Eigenvariables, bracketing and the decidability of positive minimal predicate logic
• On Long Normal Inhabitants of a Type
• Recognizability in the Simply Typed Lambda-Calculus
• Assumption Classes in Natural Deduction
• Proof normalization modulo
• Term Rewriting and Applications
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: On the expressive power of schemes