Partial inductive definitions as type-systems for -terms

DOI10.1007/BF01995106zbMATH Open0786.03011MaRDI QIDQ688729FDOQ688729

Daniel Fredholm, Svetozar Serafimovski

Publication date: 5 May 1994

Published in: BIT (Search for Journal in Brave)

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

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

• LCF considered as a programming language
• Title not available (Why is that?)
• Title not available (Why is that?)
• Partial inductive definitions
• A Proof-Theoretic Approach to Logic Programming. I. Clauses as Rules
• Title not available (Why is that?)
• A Proof-Theoretic Approach to Logic Programming

Cited In (11)

• On systems of definitions, induction and recursion
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• On the \(\lambda Y\) calculus
• Important Issues in Foundational Formalisms
• Title not available (Why is that?)
• Title not available (Why is that?)
• A term calculus for (co-)recursive definitions on streamlike data structures
• The insensitivity theorem for nonreducing reflexive types
• Title not available (Why is that?)

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)