Verified Representations of Landau's "Grundlagen" in the lambda-delta Family and in the Calculus of Constructions
Landau's "Grundlagen der Analysis" formalized in the 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 discuss an implemented procedure producing a faithful...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
University of Bologna
2016-01-01
|
| Series: | Journal of Formalized Reasoning |
| Subjects: | |
| Online Access: | https://jfr.unibo.it/article/view/4716 |