λBLL∞: Beyond polynomial time in presence of randomized computation

In this thesis we introduce the λBLL∞ calculus, a purely functional graded calculus designed for the formal analysis of mixed complexity probabilistic computation. Building upon the foundations of Bounded Linear Logic (BLL), we propose two significant extensions: the removal of stateful effects in favour of a pure functional semantics, and the expansion of the resource-accounting algebra to include exponential grades and a symbolic infinite limit. We provide a complete formal characterization of the system, including a small step operational semantics based on a sub-stochastic monad to correctly capture both probabilistic branching and potential divergence. We establish the internal consistency of λBLL∞ through exhaustive proofs of substitution and subject reduction. Furthermore, we present a soundness theorem demonstrating that the grades assigned by the type system serves as a sound complexity certificate for membership in PTIME and EXPTIME fragments. Finally, we develop a simplified logical metric based on statistical distance and apply it to cryptographic case studies. We demonstrate that λBLL∞ can formally characterize the “Security Gap” of a protocol, proving that the resource grade of an observer context serves as the definitive boundary for computational indistinguishability.