Antonio Rios

The aim of this writing is to show the similarities between the philosophy of a modern author, like Leibniz, and the philosophy of a medieval jewish author, like Maimonides. I am going to write about the concept of "substance" in both authors, looking into the similarity between the "monad" of Leibniz and the idea of "angel" of Maimonides. Both of them, "monad" and "angel", settle, not only the concept of "substance", but also the concept of "Structure of living" besides some more interesting cognitive notions which I am going to inguire into.

Calculi of explicit substitutions have almost always been presented using de Bruijn indices with the aim of avoiding α-conversion and being as close to machines as possible. De Bruijn indices however, though very suitable for the machine, are difficult to human users. This is the reason for a renewed interest in systems of explicit substitutions using variable names. We believe that the study of these systems should not develop without being well-tied to existing work on explicit substitutions. The aim of this paper is to establish a bridge between explicit substitutions using de Bruijn indices and using variable names and to do so, we provide the λt-calculus: a λ-calculus a la de Bruijn which can be translated into a λ-calculus with explicit substitutions written with variable names. We present explicitly this translation and use it to obtain preservation of strong normalisation for λt. Moreover, we show several properties of λt, including confluence on closed terms and efficiency to simulate β-reduction. Furthermore, λt is a good example of a calculus written in the λs-style that possesses the updating mechanism of the calculi á la λσ