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