How can you define the notion of "state" using only a type theory language?
I am not sure what your question exactly covers. But to have a more formal definition of "State" it could be useful to look at the State Monad in Haskell. Haskell is a functional programming language which operates different compared to a imperative programming language (like Java or C).