Fairouz Kamareddine

Historically functions have been treated as a kind of meta-object. This all changed with the work of Frege, Russell and Church. Furthermore, the challenges of the paradoxes led to the formalisation of type theory by Russell. Since, functions and...

Mathematical texts can be computerised in many ways. At one end there is document imaging, at the other there are proof assistants (Mizar, Isabelle, Coq, etc.).In between, there are typesetting (e.g., LaTeX and MathML) and semantically oriented (e.g...