Intrinsic reasoning about functional programs. II: Unipolar induction and primitive-recursion
From MaRDI portal
Publication:1827398
DOI10.1016/J.TCS.2003.11.002zbMath1046.03015OpenAlexW1999297774MaRDI QIDQ1827398
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
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