Partial inductive definitions as type-systems for \(\lambda\)-terms

DOI10.1007/BF01995106zbMath0786.03011MaRDI QIDQ688729

Daniel Fredholm, Svetozar Serafimovski

Publication date: 5 May 1994

Published in: BIT (Search for Journal in Brave)

zbMATH Keywords

lambda calculusnatural deduction calculusChurch-Rosser propertynon-normalizable deductionspartial inductive definitiontyped fixed-point operator

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Cites Work

• Partial inductive definitions
• LCF considered as a programming language
• A Proof-Theoretic Approach to Logic Programming. I. Clauses as Rules
• A Proof-Theoretic Approach to Logic Programming
• Unnamed Item
• Unnamed Item
• Unnamed Item