Intrinsic reasoning about functional programs. II: Unipolar induction and primitive-recursion

DOI10.1016/J.TCS.2003.11.002MaRDI QIDQ1827398zbMATH OpenOpenAlexFDO

Authors Daniel M. Leivant

Publication date 6 August 2004

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.tcs.2003.11.002

zbMATH Keywords

intrinsic theoriesprimitive-recursive functionsunipolar induction

Mathematics Subject Classification ID

Logic in computer science (03B70) Recursive functions and relations, subrecursive hierarchies (03D20) Functional programming and lambda calculus (68N18)

Recommendations

• Intrinsic reasoning about functional programs. I: First order theories
• A proof-theoretic account of primitive recursion and primitive iteration
• scientific article; zbMATH DE number 432705
• Computer Science Logic
• Term rewriting theory for the primitive recursive functions

Cites work

• A short proof of the strong normalization of classical natural deduction with disjunction
• Fragments of HA based on \(\Sigma_ 1\)-induction
• scientific article; zbMATH DE number 3904585 (Why is no real title available?)
• scientific article; zbMATH DE number 1226875 (Why is no real title available?)
• scientific article; zbMATH DE number 1497485 (Why is no real title available?)
• scientific article; zbMATH DE number 227056 (Why is no real title available?)
• scientific article; zbMATH DE number 2242587 (Why is no real title available?)
• scientific article; zbMATH DE number 3073037 (Why is no real title available?)
• Intrinsic reasoning about functional programs. I: First order theories
• Normalization theorems for full first order classical natural deduction
• On the proof theory of the intermediate logic MH

Cited in

(2)

• scientific article; zbMATH DE number 432705 (Why is no real title available?)
• A proof-theoretic account of primitive recursion and primitive iteration

This page was built for publication: Intrinsic reasoning about functional programs. II: Unipolar induction and primitive-recursion

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