The original lambda calculus had no type system at all, it was just a term rewriting system of variables and lambda abstractions with two rules: (\lambda a.M)N

The original lambda calculus had no type system at all, it was just a term rewriting system of variables and lambda abstractions with two rules: (\lambda a.M)N --> M[N/a] (\lambda a.M a) --> M In this sense we can say it is "dynamically typed" in that it has a single type, the type of lambda terms, although this seems like it sells short the memory safety guarantees associated to types in modern dynamically typed languages. This is the system that comes to mind for me when I think of "lambda calculus" because it is the one that was most important in the history of computability and logic, it can express the same computable functions as Turing machines. System F is not Turing complete.