vai al contenuto della pagina vai al menu di navigazione
 

Landau's "Grundlagen der Analysis" from Automath to lambda-delta

F. Guidi

UBLCS-2009-16

University of Bologna (Italy). Department of Computer Science.

L.S. van Benthem Jutting's specification of E.G.H.Y. Landau's "Grundlagen der Analysis" in the formal language Aut-QE represents an early milestone in computer-checked mathematics and is the only non-trivial development finalized in the languages of the Automath family. Here we report on our first attempt to encode this specification into the formal language lambda-delta and to validate the resulting data set against lambda-delta's type system. Our main achievement is the implementation of a software processor that takes care of all the translation-related issues, including the validation and the long-term persistence of the translated data. In this respect, the present paper fits in a research thread that aims at improving lambda-delta by testing its capability to encode real-world formal mathematics a reasonable manner.