AUTOMATH(ID:491/aut026)Eindhoven, Netherlands. A very high level language for writing proofs. The first type-theoretical proof system. AUTOMATH genealogy is hard to grasp - it was conceived as an extended project, with some languages as partial goals for that project. AUTOMATH had a subset PAL, for which SEMIPAL was an intentional precursor. That evolved into SEMIPAL 2, without becoming PAL, which emerged separately. AUT-QE and AUT-PI were forms of writing the full AUTOMATH. Related languages
References: in Symp on Automatic Demonstration, LNM 125, Springer 1970. view details in Symp on Automatic Demonstration, LNM 125, Springer 1970. view details in Symp on Automatic Demonstration, LNM 125, Springer 1970. view details in Symp on Automatic Demonstration, LNM 125, Springer 1970. view details Logic of Programming versus Logic of Mathematics We investigate the logic of programming because it will help us understand the programming process and enable us to be better at it. This "self-improvement" motive is not the typical reason why people study the logic of mathematics; and traditional logic is not always a good role model for programming logic. Why is there this difference, and does it matter? The chief reason for the difference is the computer. Programming is a formal activity unlike the "doing" of most other mathematics. It requires communication with unintelligent machines, which do not understand wonderful mathematical solutions to problems. A solution must be programmed, and this means formalized. Although the solution may be a function and hence similar in its form and precision to solutions in analysis and algebra, its description tends to be rather long by comparison with function descriptions in mathematics--say, a page or two instead of a line or two. More significantly, the exacting requirements of formality and the inherently arbitrary nature of programming formalisms make it very difficult for people to check every detail of these long solutions. In addition, features of programming languages introduced to allow efficient execution of programs complicate explanations of the solution by involving the eccentricities of a specific formalism. Confronted with these difficulties, computer scientists have been seeking logics that will explain programming solutions and permit mechanical help in finding, checking, and changing them. As it becomes more important to know that a program really does what it is claimed to do, that is, meet its specification, more details of the explanation are made explicit and formalized. The limit of this process is a completely formal proof that the program is correct. The program can be seen as the "executable part" of this proof (see [13]). The more formal the explanation of a program, the greater the opportunity to use the computer to check or help generate it. This reflexive use of the computer to check itself is one of the most intriguing and promising areas of research into the problems of "software reliability" and into the nature of the programming process itself. These incentives to produce formal algorithmic proofs seem to be much higher than any incentive to do the same for mathematical arguments with no computational content. Nevertheless, one of the earliest and most significant efforts to actually use formal proofs was in the AUTOMATH project at Eindhoven in the Netherlands under the direction of N. G. deBruijn [14]. The goal of the project was to write formal mathematical proofs and check them by a computer program. DeBruijn imposed, by desire, the standards of extreme exactness that arise, by necessity, in programming. The chief characteristics of AUTOMATH and the programming logics is that they are meant to be used, whereas the formal theories presented in logic textbooks are meant to be studied. This difference is crucial and is the driving force behind AUTOMATH as well as PL/CV [8, 11] and PRL [2, 3]. This characteristic means that the logic must be sufficiently expressive that it naturally captures all the informal arguments in the subject being considered. We claim that the V3 described here enjoys such expressiveness. in Symp on Automatic Demonstration, LNM 125, Springer 1970. view details This paper gives what the authors call a "succinct, yet thorough" presentation of the core of PL/CV3. The core is based on type theory and much of the presentation is concerned with constructing a type hierarchy. The introduction of operators that permit the decomposition of an object into its intentional structure allows for the analy. of the concept of type within the theory, itself. So operators are not present in, e.g., Marin-Lof's intuitionistic type theory, but the introduction of intensionality is reminiscent of Russell's ramified type theory. The last section the paper consists of applications of the theory to constructive logic, the integers, and lists. in Symp on Automatic Demonstration, LNM 125, Springer 1970. view details in Symp on Automatic Demonstration, LNM 125, Springer 1970. view details in Symp on Automatic Demonstration, LNM 125, Springer 1970. view details |