Intrinsic reasoning about functional programs. I: First order theories

DOI10.1016/S0168-0072(01)00078-1zbMath0992.03037MaRDI QIDQ5957855

Daniel Leivant

Publication date: 2 June 2002

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

zbMATH Keywords

natural deductionfree algebras\(\lambda\)-calculusCurry-Howard morphismsequational programsfirst-order arithmeticintrinsic theoriesreasoning about functional programsstrong normalization theorem

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Complexity of computation (including implicit computational complexity) (03D15) Cut-elimination and normal-form theorems (03F05) First-order arithmetic and fragments (03F30) Complexity classes (hierarchies, relations among complexity classes, etc.) (68Q15) Complexity of proofs (03F20)

Related Items (4)

Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control ⋮ 2003 Annual Meeting of the Association for Symbolic Logic ⋮ An arithmetic for non-size-increasing polynomial-time computation ⋮ Intrinsic reasoning about functional programs. II: Unipolar induction and primitive-recursion

Cites Work

• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Intrinsic reasoning about functional programs. I: First order theories