First we will discuss models, we will discuss three fundamental and universal computational models. The first as I said is l-calculus, which is the foundational underpinning of sequential computation and functional programming.
Then we have typed l-calculus, which is precisely a tool for representing formal reasoning: it is the combination of tight theory with l-calculus. So typed l-calculus is equal to l-calculus plus type theory.
And then we have the p-calculus: this is a model for representing concurrent and mobile computation.
