H ? « ‹ ← → › »

Language peer sets for AUTOMATH:
Netherlands↑
Netherlands/1967↑
Designed 1967 ↑
1960s languages ↑
Third generation↑
High Cold War↑
Genus Algebraic ↑
Specialised Languages ↑
Algebraic↑
Mathematical↑
Expression-oriented ↑
Algebraic/1967↑
Mathematical/1967↑
Expression-oriented/1967↑
Algebraic/Netherlands↑
Mathematical/Netherlands↑
Expression-oriented/Netherlands↑
Specialised Languages ↑
Specialised Languages/1967↑
Specialised Languages/NL ↑

AUTOMATH(ID:491/aut026)

alternate simple view
Country: Netherlands
Designed 1967
Published: 1968
Genus: Algebraic
Sammet category: Specialised Languages

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
AUTOMATH → SEMIPAL   Subset
References:
  • de Bruijn, N.G. (1970) de Bruijn, N.G. "The Mathematical Language AUTOMATH, Its Usage and Some of its Extensions"
          in (1970) Symp on Automatic Demonstration, LNM 125, Springer 1970.
  • Jutting, L.S. Checking Landau's (1979) Jutting, L.S. Checking Landau's "Grundlagen' in the AUTOMATH system. Doctoral dissertation, Eindhoven Univ., Math. Centre Tracts 83, Math. Centre, Amsterdam, 1979
          in (1970) Symp on Automatic Demonstration, LNM 125, Springer 1970.
  • de Bruijn, Nicolas G. (1980) 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.
          in (1970) Symp on Automatic Demonstration, LNM 125, Springer 1970.
  • Nederpelt, R. P. (1980) Nederpelt, R. P. "Selected Papers on Automath" Elsevier 1980
          in (1970) Symp on Automatic Demonstration, LNM 125, Springer 1970.
  • Constable, Robert L. and Zlatin, Daniel R. (1984) 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 Abstract DOI Extract: Logic of Programming versus Logic of Mathematics
          in (1970) Symp on Automatic Demonstration, LNM 125, Springer 1970.
  • McLean, J. (1984) McLean, J. D. review of Constable and Zlatin 1984 in ACM Computing Reviews August 1984 Abstract
          in (1970) Symp on Automatic Demonstration, LNM 125, Springer 1970.
  • Barendregt, H.; Rezus, A. (1985) Barendregt, H.; Rezus, A. "Semantics for classical AUTOMATH and related systems" Inf. Control 59, 1-3 pp127-147.
          in (1970) Symp on Automatic Demonstration, LNM 125, Springer 1970.
  • Kamareddine, Fairouz (ed) (2004) 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) Abstract Web page for conference
          in (1970) Symp on Automatic Demonstration, LNM 125, Springer 1970.
    Search in: Google  Google scholar  World Cat  Yahoo  Overture  DBLP  Monash bib  NZ  IEEE  ACM portal  CiteSeer  CSB  ncstrl  jstor  Bookfinder