Partial inductive definitions as type-systems for -terms

DOI10.1007/BF01995106MaRDI QIDQ688729zbMATH OpenFDO

Authors 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)

Recommendations

• Typed λ-calculus with recursive definitions
• scientific article; zbMATH DE number 512879
• scientific article; zbMATH DE number 891219
• On systems of definitions, induction and recursion
• Some lambda calculi with categorical sums and products

Cites work

• scientific article; zbMATH DE number 3993540 (Why is no real title available?)
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• scientific article; zbMATH DE number 3365218 (Why is no real title available?)
• A Proof-Theoretic Approach to Logic Programming
• A Proof-Theoretic Approach to Logic Programming. I. Clauses as Rules
• LCF considered as a programming language
• Partial inductive definitions

Cited in

(13)

• On systems of definitions, induction and recursion
• scientific article; zbMATH DE number 3928341 (Why is no real title available?)
• scientific article; zbMATH DE number 4134038 (Why is no real title available?)
• On the \(\lambda Y\) calculus
• scientific article; zbMATH DE number 65538 (Why is no real title available?)
• Important Issues in Foundational Formalisms
• scientific article; zbMATH DE number 1424053 (Why is no real title available?)
• Ellipses and lambda definability
• scientific article; zbMATH DE number 3557747 (Why is no real title available?)
• A term calculus for (co-)recursive definitions on streamlike data structures
• Type fixpoints, iteration vs. recursion
• The insensitivity theorem for nonreducing reflexive types
• scientific article; zbMATH DE number 3928339 (Why is no real title available?)

This page was built for publication: Partial inductive definitions as type-systems for \(\lambda\)-terms

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