Automath List

Click here to sort the list on: number, date, author, title
Some articles are offline until copyright issues are cleared.

Nr. Year Author(s) Title
AUT036A 1974 Zandleven, I. <no title>
AUT035 1973 Daalen, D.T. van A description of AUTOMATH and some aspects of its language theory
AUT040 1974 Bruijn, N.G. de A framework for the description of a number of members of the AUTOMATH family
AUT059 1978 Bruijn, N.G. de A namefree lambda calculus with facilities for internal definition of expressions and segments
AUT050 1977 Bruijn, N.G. de A namefree lambda calculus with formulas involving symbols that represent reference transforming mappings
AUT024 1971 Benthem Jutting, L.S. van A normal form theorem in lambda calculus with types
AUT057 1978 Bruijn, N.G. de A note on weak diamond properties
AUT004 1970 Bruijn, N.G. de A processor for PAL
AUT072 1980 Bruijn, N.G. de A survey of the project AUTOMATH
AUT033 ? Bruijn, N.G. de A system for handling syntax and semantics of computer programs in terms of the mathematical language AUTOMATH
AUT068 1979 Nederpelt, R.P. A system of lambda-calculus possessing facilities for typing and abbreviating, Part I: Informal introduction
AUT075 1980 Nederpelt, R.P. A system of lambda-calculus possessing facilities for typing and abbreviating, Part II: Formal description
AUT071 1980 Nederpelt, R.P. A system of natural reasoning based on a typed lambda calculus (abstract)
AUT033A 1973 Bruijn, N.G. de A technique for deriving semantic information on computer programs
AUT069 1980 Udding, J.T. A Theory of Real Numbers and its Presentation in AUTOMATH, Vol. I-III
AUT060 1976 Benthem Jutting, L.S. van A translation of Landau's "Grundlagen" in AUTOMATH, Vol. 1-5
AUT088 1984 Braun, W.C.P. A translator for AUTOMATH and its implementation in Pascal
AUT036 1973 Zandleven, I. A Verifying Program for AUTOMATH
AUT076 1980 Nederpelt, R.P. An approach to theorem proving on the basis of a typed lambda calculus
AUT089 1984 Leijnen, A. An interactive program for checking the correctness of expressions in AUT-SL
AUT039 1974 Bruijn, N.G. de AUTOMATH - ein Project zur Kontrolle von Mathematik
AUT019 1970 Nederpelt, R.P. AUTOMATH, a language for checking mathematics with a computer
AUT001 1968 Bruijn, N.G. de AUTOMATH, a language for mathematics
AUT030 1973 Bruijn, N.G. de AUTOMATH, a language for mathematics
AUT056 1978 Bruijn, N.G. de AUT-QE without type inclusion
AUT020 1971 Bruijn, N.G. de AUT-SL, a single line version of AUTOMATH
AUT080 1981 Benthem Jutting, L.S. van Beschrijving van AUT-68
AUT062 1975 Nederpelt, R.P. Bewijsmethoden
AUT063 1978 Nederpelt, R.P. Bewijszinnen
AUT038 1975 Vrijer, R.C. de Big trees in a lambda calculus with lambda expressions as types
AUT046 1977 Benthem Jutting, L.S. van Checking Landau's "Grundlagen" in the AUTOMATH system (External Link)
AUT099 1986 Bruijn, N.G. de Checking mathematics with the aid of computer
AUT007 1970 Bruijn, N.G. de Coding System for AUT-QE
AUT087 1983 Bruijn, N.G. de Computer program semantics in space and time
AUT085 1983 Gestel, L.F.M. van Computerprogramma's; hun semantiek in AUTOMATH. Een vergelijking tussen ideeen van Bruijn, N.G. de uit 1973 en de uitwerking daarvan door R. Wieringa
AUT098 1985 Nederpelt, R.P. De ideeen achter AUTOMATH
AUT011 1970 Bruijn, N.G. de Definitions of limits in AUTOMATH
AUT083 1982 Benthem Jutting, L.S. van Description of language definition and verifier for Aut-68 and AUT-QE, with treatment of strings and telescopes
AUT053 1977 Nederpelt, R.P. Een aanzet tot bewijsanalyse
AUT047A 1973 Zandleven, I. Een indeling van AUTOMATH teksten in paragrafen en het herhaalde gebruik van namen
AUT058 1978 Wieringa, R.M.A. Een notatie-systeem voor lambda-calculus met definities
AUT079 1980 Benthem Jutting, L.S. van, Donkers J.G.M.,
Meeuwen, W.H.J.H. van Nederpelt, R.P.,
Nieuwkasteele, C.P. van,
Udding, J.T.
Ervaringen met de wiskundige omgangstaal WOT
AUT012 1970 Benthem Jutting, L.S. van Example of a text in the formal language AUTOMATH
AUT010 1968 Bruijn, N.G. de Example of a text written in AUTOMATH
AUT013 1970 Benthem Jutting, L.S. van Example of a text written in AUT-QE
AUT042 1975 Zucker, J. Formalization of classical mathematics in AUTOMATH
AUT086 1984 Bruijn, N.G. de Formalization of constructivity in AUTOMATH
AUT008 1970 Bruijn, N.G. de Formulas with indications for establishing definitional equivalence
AUT092 1987 Bruijn, N.G. de Generalizing AUTOMATH by means of a lambda-typed lambda calculus
AUT065 1979 Bruijn, N.G. de Grammatica van WOT
AUT043 1976 Bruijn, N.G. de Het AUTOMATH project
AUT028 1972 Daalen, D.T. van Interpretatie- en consistentieproblemen in AUTOMATH
AUT093 1987 Balsters, H. Lambda calculus extended with segments
AUT100 1986 Balsters, H. Lambda Calculus extended with Segments
AUT029 1972 Bruijn, N.G. de Lambda Calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem
AUT055 1978 Bruijn, N.G. de Lambda calculus with namefree formulas involving symbols that represent reference transforming mappings
AUT021 1971 Nederpelt, R.P. Lambda-Automath
AUT022 1971 Nederpelt, R.P. Lambda-Automath II
AUT017 1969 Bruijn, N.G. de Machinale verificatie van redeneringen
AUT052 1977 Bruijn, N.G. de Materiaal uitgereikt bij college Wiskundige Talen
AUT084 1982 Bruijn, N.G. de Materiaal uitgereikt bij het college Wiskundige Talen
AUT082 1981 Donkers, J.G.M. Mathematical Vernacular: an introduction
AUT045 1976 Bruijn, N.G. de Modifications of the 1968 version of AUTOMATH
AUT101 1986 Benthem Jutting, L.S. van Normalization in Coquand's system
AUT049 1977 Bruijn, N.G. de Notation for concatenation
AUT023 1971 Benthem Jutting, L.S. van On normal forms in AUTOMATH
AUT006 1970 Bruijn, N.G. de On the use of bound variables in AUTOMATH
AUT048 1977 Zandleven, I. On the use of identifiers in AUT-PI
AUT091 1984 Nederpelt, R.P. Over de taal van de wiskunde
AUT054 1977 Nederpelt, R.P. Presentation of natural deduction
AUT074 1980 Bruijn, N.G. de Recommendations concerning standardization of mathematical formulas
AUT081 1980 Wieringa, R.M.A. Relational semantics in an integrated system
AUT070 1979 Benthem Jutting, L.S. van,
Wieringa, R.
Representatie van expressies in het verificatieprogramma VERA 79
AUT003 1969 Bruijn, N.G. de SEMIPAL 2, an extension of the mathematical language SEMIPAL
AUT078 1983 Nederpelt, R.P. Sentences in the language of reasoning
AUT032 1973 Bruijn, N.G. de Set theory with type restrictions
AUT077 1980 Nederpelt, R.P. Signaalwoorden in bewijstaal
AUT025 1972 Bruijn, N.G. de Some abbreviations in the input language for AUTOMATH
AUT051 1977 Bruijn, N.G. de Some auxiliary operators in AUT-PI
AUT044 1974 Bruijn, N.G. de Some extensions of AUTOMATH: the AUT-4 family
AUT102 1988 Nederpelt, R.P. Some remarks on typed lambda calculi with a view to the formalization of mathematics
AUT026 1972 Nederpelt, R.P. Strong normalization in a lambda-calculus with lambda-expressions as types
AUT031 1973 Nederpelt, R.P. Strong normalization in a typed lambda calculus with lambda structured types
AUT009 1970 Benthem Jutting, L.S. van Synopsis of the definition of the language AUTOMATH, extracted from lectures of Bruijn, N.G. de
AUT061 1984 Bruijn, N.G. de Taal en Structuur van de Wiskunde
AUT103A 1974 Bruijn, N.G. de Telescopic Mappings
AUT103 1991 Bruijn, N.G. de Telescopic Mappings in a Typed Lambda Calculus
AUT034 1973 Bruijn, N.G. de The AUTOMATH Mathematics Checking Project
AUT027 1972 Nederpelt, R.P. The closure theorem in lambda-typed lambda-calculus
AUT037 1973 Benthem Jutting, L.S. van The development of a text in AUT-QE
AUT090 1984 Benthem Jutting, L.S. van The language theory of /\, a typed lambda calculus where terms are types
AUT073 1980 Daalen, D.T. van The language theory of AUTOMATH (External Link)
AUT002 1968 Bruijn, N.G. de The mathematical language AUTOMATH
AUT097 1982 Nederpelt, R.P. The signal value of words in mathematical phrasing
AUT005 1970 Bruijn, N.G. de The Syntax of PAL and AUTOMATH
AUT047 1977 Zandleven, I. The use of paragraphs in AUTOMATH
AUT041 1975 Bruijn, N.G. de The use of the language AUTOMATH for syntax and semantics of programming languages
AUT096 ? Nederpelt, R.P. Uber den Begriff der Bindung in der mathematischen Sprache
AUT094 1985 Bruijn, N.G. de Upper bound for the length of the norm of an expression in lambda-typed lambda calculus
AUT095 1985 Bruijn, N.G. de Upper bounds for the length of normal forms and for the length of reduction sequences in lambda-typed lambda calculus
AUT066 1980 Bruijn, N.G. de Van alles en nog wat over gebonden variabelen in wiskundige taal
AUT016 1967 Bruijn, N.G. de Verificatie van Wiskundige Bewijzen door een Computer
AUT018 1969 Bruijn, N.G. de Verification des textes mathematiques par un ordinateur
AUT015 1970 Daalen, D.T. van Verzamelingstheorie, de axioma's van Zermelo-Fraenkel
AUT014 1970 Daalen, D.T. van Verzamelingstheorie, een intuitieve opzet
AUT064 1979 Bruijn, N.G. de Wees contextbewust in WOT
AUT067 1980 Bruijn, N.G. de Wiskundigen, let op uw Nederlands