In the 1970s van Benthem Jutting translated Landauís book Grundlagen der Analysis into Automath. The type theory of Automath differs from modern type theories in significant ways. The most important difference is that Automath is λ-typed while most modern type theories are Π-typed. In this paper we define the notion of a faithful reproduction of an Automath signature. We describe how one can obtain a particular faithful reproduction of a signature corresponding to the Automath version of Landauís book. We then consider what properties a Π-typed type theory must have in order for the faithful reproduction to be a correct signature. Based on this information, we can give different mappings of the reproduction into type theories such as ECC and, in particular, the system Coq.
Download PDF Show BibTeX
Login to edit