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
AUTOMATH => aut   Evolution of
AUTOMATH => AUT-68   Implementation
AUTOMATH => AUT-PI   Implementation
AUTOMATH => AUT-QE   Implementation
AUTOMATH => coq   Based on
AUTOMATH => PAL   Partial subset of
AUTOMATH => PVS   Influence

  • de Bruijn, N.G. "The Mathematical Language AUTOMATH, Its Usage and Some of its Extensions" view details
          in Symp on Automatic Demonstration, LNM 125, Springer 1970. view details
  • Jutting, L.S. Checking Landau's "Grundlagen' in the AUTOMATH system. Doctoral dissertation, Eindhoven Univ., Math. Centre Tracts 83, Math. Centre, Amsterdam, 1979 view details
          in Symp on Automatic Demonstration, LNM 125, Springer 1970. view details
  • de Bruijn, Nicolas G. "A survey of the project AUTOMATH" In J. P. Seldin and J. R. Hindley, editors, To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus, and Formalism, pages 589--606, Academic Press, 1980. view details
          in Symp on Automatic Demonstration, LNM 125, Springer 1970. view details
  • Nederpelt, R. P. "Selected Papers on Automath" Elsevier 1980 view details
          in Symp on Automatic Demonstration, LNM 125, Springer 1970. view details
  • Constable, Robert L. and Zlatin, Daniel R. "The Type Theory of PL/CV3" ACM Transactions on Programming Languages and Systems (TOPLAS) 6(1) (January 1984) pp94-117 view details Abstract: The programming logic PL/CV3 is based on the notion of a mathematical type. The core of the type theory, from which the full theory for program verification and specification can be derived, is presented. Whereas the full theory was designed to be usable, the core theory was selected to be analyzable. This presentation strives to be succinct, yet thorough. The last section consists of examples, but the approach here is not tutorial. DOI Extract: Logic of Programming versus Logic of Mathematics
    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
  • McLean, J. D. review of Constable and Zlatin 1984 in ACM Computing Reviews August 1984 view details Abstract: A programming logic is a formal theory for analyzing programs. PL/CV3 is a programming logic designed to steer a course between the Scylla of predicate calculus, which the authors regard as insufficiently expressive to be usable, and the Charybdis of stronger formalisms, such as AUTOMATH or set theory, which the authors regard as having too much noncomputational baggage. The passage is narrow, indeed, since presumably, the authors regard first-order formulations of set theory as both insufficiently expressive and over-baggaged.

    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
  • Barendregt, H.; Rezus, A. "Semantics for classical AUTOMATH and related systems" Inf. Control 59, 1-3 pp127-147. view details
          in Symp on Automatic Demonstration, LNM 125, Springer 1970. view details
  • Kamareddine, Fairouz (ed) "Thirty-Five Years of Automating Mathematics: A Volume Dedicated to de Bruijn's Automath" Applied Logic Series, V. 28 Kluwer Academic Publishers; (February 2004) view details Abstract: N.G. de Bruijn was a well established mathematician before deciding in 1967 at the age of 49 to work on a new direction related to Automating Mathematics. In the 1960s he became fascinated by the new computer technology and decided to start the Automath project where he could check, with the help of the computer, the correctness of books on mathematics. Through his work on Automath de Bruijn started a revolution in using the computer for verification, and since, we have seen more and more proof-checking and theorem-proving systems. Automath was written in Algol 60 and implemented on the primitive computers of the sixties. Thirty years on, both technology and theory have evolved a lot leading to impressive new directions in using the computer for manipulating and checking mathematics. This volume is a collection of papers with a personal flavour. It consists of 11 articles which propose interesting variations to or examples of mechanising mathematics and illustrate differ developments in symbolic computation in the past 35 years. The first paper is by de Bruijn himself where he uses his experience of automating mathematics to reason about the human mind. After that a number of intriguing articles have been contributed by amongst others Henk Barendregt, who proposes a mathematical proof language between informal and formalised mathematics which helps make proof assistants more user friendly, and Robert Constable, explaining how Automath's telescopes, books and definitions compare to recent developments in computational type theory made by his Nuprl group. The volume further includes a strong argumentation by Arnon Avron that for automated reasoning, there is an interesting logic, somewhere strictly between first and second order logic, determined essentially by an analysis of transitive closure, yielding induction; and Murdoch Gabbay presenting an interesting generalisation of Fraenkel-Mostowski (FM) set theory within higher-order logic, and applying it to model Milner's p-calculus External link: Web page for conference
          in Symp on Automatic Demonstration, LNM 125, Springer 1970. view details