Typing in reflective combinatory logic

DOI10.1016/J.APAL.2005.11.004MaRDI QIDQ2498910zbMATH OpenOpenAlexFDO

Authors Nikolai Krupski

Publication date 16 August 2006

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.2005.11.004

zbMATH Keywords

proof theoryderivabilitytypingwell-formed formulacomplexity, cut eliminationreflective combinatory logic

Mathematics Subject Classification ID

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

Recommendations

• Restoration of types in reflexive combinatory logic
• Strong normalization and confluence for reflexive combinatory logic
• Principal type-schemes and condensed detachment
• Reflection in rewriting logic. Metalogical foundations and metaprogramming applications
• Reflection in conditional rewriting logic
• Theorem Proving in Higher Order Logics
• scientific article; zbMATH DE number 432706
• scientific article; zbMATH DE number 1231667
• scientific article; zbMATH DE number 2063228
• scientific article; zbMATH DE number 2006628

Cites work

• scientific article; zbMATH DE number 1215502 (Why is no real title available?)
• scientific article; zbMATH DE number 1302061 (Why is no real title available?)
• scientific article; zbMATH DE number 1776257 (Why is no real title available?)
• scientific article; zbMATH DE number 949290 (Why is no real title available?)
• scientific article; zbMATH DE number 2209442 (Why is no real title available?)
• Alternation
• Explicit provability and constructive semantics
• Intuitionistic propositional logic is polynomial-space complete
• Kolmogorov and Gödel's approach to intuitionistic logic: current developments

Cited in

(8)

• Combinatory logic with polymorphic types
• scientific article; zbMATH DE number 785045 (Why is no real title available?)
• Sequent Calculus for Intuitionistic Epistemic Logic IEL
• scientific article; zbMATH DE number 1265030 (Why is no real title available?)
• Restoration of types in reflexive combinatory logic
• Strong normalization and confluence for reflexive combinatory logic
• The basic intuitionistic logic of proofs
• scientific article; zbMATH DE number 6304248 (Why is no real title available?)

This page was built for publication: Typing in reflective combinatory logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2498910)