2013/01/13 by Satoshi Matsuoka, Matsuoka, Satoshi
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Programming Languages (cs.PL) #cs.LO #cs.PL #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.1301.2763
arxiv created 2013/01/13 · openalex publication_date 2013/01/13 · arxiv updated 2013/01/15 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We give a new proof of P-time completeness of Linear Lambda Calculus, which was originally given by H. Mairson in 2003. Our proof uses an essentially different Boolean type from the type Mairson used. Moreover the correctness of our proof can be machined-checked using an implementation of Standard ML.