×
Dechesne, Francien; Nederpelt, Rob

N. G. de Bruijn (1918–2012) and his road to Automath, the earliest proof checker. (English) Zbl 1257.01016

Math. Intell. 34, No. 4, 4-11 (2012).

Cited in 3 Documents

MSC:

01A70 Biographies, obituaries, personalia, bibliographies
01A60 History of mathematics in the 20th century
68-03 History of computer science

Biographic References:

de Bruijn, N. G.

Software:

HOL; Automath; Isabelle; Coq; ML
Cite Review PDF
Full Text: DOI

References:

[1] Agda. http://wiki.portal.chalmers.se/agda/ .
[2] The Automath Archive. Hosted at Eindhoven University of Technology: http://www.win.tue.nl/automath/ .
[3] H. P. Barendregt. Lambda Calculi with Types. Chapter 2 (pp. 117–309) of S. Ambramsky et al. (eds.): Handbook of Logic in Computer Science, Vol. 2, Oxford University Press, 1992.
[4] H. Barendregt and H. Geuvers. Proof-Assistants using Dependent Type Systems. Chapter 18 (pp. 1149–1238) of J. A. Robinson and A. Voronkov (eds.): Handbook of Automated Reasoning, Vol. 2, Elsevier and The MIT Press, 2001. · Zbl 1005.03011
[5] L. S. van Benthem Jutting. Checking Landau’s ”Grundlagen” in the Automath System. Ph.D. thesis, Technische Hogeschool Eindhoven, 1977. · Zbl 0352.68105
[6] Aart Blokhuis and Jack van Lint. In memoriam: Johan Jacob Seidel. Nieuw Archief voor Wiskunde, 5/2(3):207–209, September 2001.
[7] N. G. de Bruijn. Over modulaire vormen van meer veranderlijken. Ph.D. thesis, Vrije Universiteit Amsterdam, 1943.
[8] N. G. de Bruijn. Eenige beschouwingen over de waarde der wiskunde (”Some observations on the value of mathematics”). Inaugural speech as professor of pure and applied mathematics and theoretical mechanics at Delft University of Technology, 1946.
[9] N. G. de Bruijn. Programmeren van de Pentomino Puzzel (”Programming the Pentomino Puzzle”). Euclides, 47:90–104, 1971/1972. · Zbl 0239.05001
[10] N. G. de Bruijn. Wiskundige modellen voor het levende brein (”Mathematical models for the living brain”). Report of the common meeting of the physics section of the KNAW, 83, No. 10, 1974.
[11] N. G. de Bruijn. Lambda calculus with namefree formulas involving symbols that represent reference transforming mappings. Indagationes Math. 40:348–356, 1978. · Zbl 0393.03009
[12] N. G. de Bruijn. Remembering Kloosterman. Nieuw Archief voor Wiskunde, 5/1(2):130–134, June 2000. · Zbl 0960.01022
[13] N. G. de Bruijn. Jaap Seidel, a friend. Nieuw Archief voor Wiskunde, 5/2(3):204–206, September 2001. · Zbl 1239.01112
[14] R. L. Constable et al. Implementing Mathematics with the Nuprl Development System, Prentice-Hall, NJ, 1986.
[15] The Coq Development Team. The Coq Proof Assistant, Reference Manual, Version 8.3. http://coq.inria.fr/refman/ .
[16] Th. Coquand and G. Huet. The calculus of constructions. Information and Computation, 76:95–120, 1988. · Zbl 0654.03045
[17] M. J. C. Gordon, T. F. Melham. Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, 1993. · Zbl 0779.68007
[18] R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. In Proceedings Second Symposium of Logic in Computer Science, Ithaca, N.Y., pp. 194–204, IEEE, Washington, DC, 1987. · Zbl 0778.03004
[19] W. A. Howard. The formulas-as-types notion of construction. In: J. P. Seldin, J. R. Hindley (eds.): To H. B. Curry: Essays on Combinatory logic, Lambda calculus and Formalism. Academic Press, pp. 479–490, 1980.
[20] Isabelle. http://isabelle.in.tum.de/ .
[21] F. Kamareddine. Thirty-five years of automating mathematics. Workshop. Kluwer Academic Publishers, Dordrecht, Boston, 2003. ISBN 1402016565. · Zbl 1055.68002
[22] E. Kamke. Theory of Sets. Dover Publications, 1950. Re-edition. · Zbl 0037.03501
[23] D. Knuth. Dancing Links. Paper P159 at http://www-cs-faculty.stanford.edu/\(\sim\)uno/preprints.html .
[24] E. Landau. Grundlagen der Analysis. First ed.: Leipzig, 1930. Third ed.: Chelsea Publ. Comp. New York, 1960. · JFM 56.0191.01
[25] Mathematics, Logic and Computation. A satellite workshop of ICALP03, in honour of N. G. de Bruijn’s 85th anniversary. 4–5 July 2003. http://www.cedar-forest.org/forest/events/Bruijn03/ .
[26] R. P. Nederpelt, J. H. Geuvers, and R. C. de Vrijer (eds.): Selected Papers on Automath, volume 133 of Studies in Logic and the Foundations of Computer Science. Elsevier, 1994. · Zbl 1359.03003
[27] B. Nordström, K. Petersson, and J. M. Smith. Programming in Martin-Löf’s Type Theory. Oxford University Press, 1990. · Zbl 0744.03029
[28] G. Plotkin. LCF considered as a programming language. Theor. Comp. Sci. 5:223–255, 1977. · Zbl 0369.68006
[29] PVS. http://pvs-wiki.csl.sri.com/index.php/Main_Page .
[30] F. Schuh. Leerboek der Elementaire Theoretische Rekenkunde (”Textbook on Elementary Theoretical Arithmetic”). Noordhoff. Part 1: De gehele getallen (”The Integers”), 1919. Part 2: De meetbare Getallen (”The Measurable Numbers”), 1921.
[31] The Twelf Project. http://twelf.plparty.org/wiki/Main_Page .
[32] N. G. de Bruijn. Asymptotic Methods in Analysis. North Holland Publishing Company and P. Noordhoff, 1958; Dover Publications, Inc., New York, 1981. · Zbl 0082.04202
[33] N. G. de Bruijn. Ein Satz über schlichte Funktionen (”A theorem on schlicht functions”). Nederl. Akad. Wetensch. Proceedings, 44:47–49, 1941. (=Indagationes Math., 3:8–10, 1941).
[34] N. G. de Bruijn. On Mahler’s partition problem. Nederl. Akad. Wetensch. Proceedings, 51: 659–669, 1948. (=Indagationes Math., 10:210–220, 1948). · Zbl 0030.34502
[35] N. G. de Bruijn. The roots of trigonometric integrals. Duke Math. J., 17:197–226, 1950. · Zbl 0038.23302
[36] N. G. de Bruijn. On bases for the set of integers. Publ. Math. Debrecen, 1:232–242, 1950. · Zbl 0038.18502
[37] N. G. de Bruijn. On the number of positive integers x and free of prime factors > y. Nederl. Akad. Wetensch. Proceedings, 53:813–821, 1950. (=Indagationes Math., 12:257–265, 1950).
[38] N. G. de Bruijn. Functions whose differences belong to a given class. Nieuw Archief Wiskunde (2) 23:194–218, 1951. · Zbl 0042.28805
[39] N. G. de Bruijn. Function theory in Banach algebras. Ann. Acad. Sci. Fennicae Ser. A. I. Math. 250/5, 1958. 12 pp. · Zbl 0082.29502
[40] N. G. de Bruijn. Generalization of Pólya’s fundamental theorem in enumerative combinatorial analysis. Nederl. Akad. Wetensch. Proceedings Ser. A 62: 59–69, 1959. (=Indagationes Math. 21). · Zbl 0085.00901
[41] N. G. de Bruijn. The mathematical language Automath, its usage, and some of its extensions. Symposium on Automatic Demonstration (Versailles, December 1968). Lecture Notes in Mathematics, vol. 125. Springer-Verlag, 1970, pp. 29–61. Reprinted in [26], pp. 73–100.
[42] N. G. de Bruijn. A theory of generalized functions, with applications to Wigner distribution and Weyl correspondence. Nieuw Archief Wiskunde (3) 21:205–280, 1973. · Zbl 0269.46033
[43] N. G. de Bruijn. Defining reals without the use of rationals. Nederl. Akad. Wetensch. Proceedings Ser. A 79:100–108, 1976. (=Indagationes Math. 36). · Zbl 0324.10054
[44] N. G. de Bruijn. Algebraic theory of Penrose’s non-periodic tilings of the plane. Nederl. Akad. Wetensch. Proceedings Ser. A 84:38–66, 1981. (=Indagationes Math. 43). Reprinted in: The Physics of Quasicrystals, P. J. Steinhardt and S. Ostlund (eds.), World Scientific Publ. Comp., Singapore, 1987, pp. 673–700. · Zbl 0457.05022
[45] N. G. de Bruijn. Can people think? Journal of Consciousness Studies, Vol. 3, 1996, pp. 425–447.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.