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

DOI10.1016/J.TCS.2003.11.002zbMath1046.03015OpenAlexW1999297774MaRDI QIDQ1827398

Daniel 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

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

Cites Work

• Fragments of HA based on \(\Sigma_ 1\)-induction
• On the proof theory of the intermediate logic MH
• Normalization theorems for full first order classical natural deduction
• A short proof of the strong normalization of classical natural deduction with disjunction
• Intrinsic reasoning about functional programs. I: First order theories
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

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