Does there exists mathematics, theoretic behind ocaml type system.
[PS : I learned recently lambda calculus is untyped ]
While this site is definitely the place I would ask an OCaml question, since your question has another foot based in the world of type theory you might also ask at the StackExchange Proof Assistants site for related information.
Lambda Calculus started without a typing system. However the ancestry of Lambda Calculus is deep and varied. (ref 1)
You might find this of interest: Solving the halting problem (Don’t let the title fool you, this is about Lambda Calculus and explains why Lambda Calculus with types is useful).
I followed a course on type systems, that was taught by someone from the research team that works on ocaml, notes are available here : http://cambium.inria.fr/~remy/mpri/cours.pdf
1 Like
The name F is coming back.
Here a language F* which is supposed to compile to F# and Ocaml,
https://www.fstar-lang.org/tutorial/