2010/02/18 by Luca Vercelli, Vercelli, Luca
Computer Science · #Computational Complexity (cs.CC) #FOS: Computer and information sciences #Formal Methods in Verification #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #cs.CC
paper · pdf · doi:10.48550/arxiv.1002.3453
PhD thesis. about 180 pages
arxiv created 2010/02/18 · openalex publication_date 2010/02/18 · arxiv updated 2010/02/26 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Our primary motivation is the comparison of two different traditions used in ICC to characterize the class FPTIME of the polynomial time computable functions. On one side, FPTIME can be captured by Intuitionistic Light Affine Logic (ILAL), a logic derived from Linear Logic, characterized by the structural invariant Stratification. On the other side, FPTIME can be captured by Safe Recursion on Notation (SRN), an algebra of functions based on Predicative Recursion, a restriction of the standard recursion schema used to defiine primitive recursive functions. Stratifiication and Predicative Recursion seem to share common underlying principles, whose study is the main subject of this work.