F. Guidi, “Verified Representations of Landau’s ‘Grundlagen’ in the lambda-delta Family and in the Calculus of Constructions”, JFR, vol. 8, no. 1, pp. 93–116, Jan. 2015.