Guidi, F. Verified Representations of Landau’s "Grundlagen" in the Lambda-Delta Family and in the Calculus of Constructions. JFR 2015, 8, 93-116.