Alejandra Ríos Ramírez

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 λσ

From the reconstruction of the approaches of Rodrigo Uprimny and Rajeev Bhargava on transitional justice models, it will be posed that the minimally decent society concept, coined by the second author, sheds new light on the discussions about better models to be implemented in societies with humanitarian crises. Intertwining the arguments of these authors could allow us to extend the scope of application of transitional justice to diverse contexts, say from dictatorship to democracy, from war to peace, or from a barbaric society to a minimally decent one.