This paper relates two distinct traditions: the one of complexity classes characterisations through light logics and models
of nondeterminism. Light logics provide an implicit characterisation of P-Time algorithms through the Curry-Howard isomorphism:
every derivation reduces to its normal form in polynomial time and every polynomial Turing machine can be simulated by a derivation.
In this paper, we extend Intuitionistic Light Affine Logic, a logic with full weakening, with a simple rule for nondeterminism
and get a completeness result for NP-Time algorithms which is, as far as we know, the first Curry-Howard characterisation
of NP complexity. We conclude by a reformulation of the P ≠ NP conjecture.
Keywords Light logics - implicit characterisations of complexity classes - NP complexity