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