This volume contains the Proceedings of the workshop on
Mathematics, Logic and Computation (MLC03) held in Eindhoven, the
Netherlands on July 4 and 5, 2003, as a satellite event of ICALP'2003.
N.G. de Bruijn was born on July 9, 1918. He finished school at the age
of 16, studied Mathematics at Leiden University and received his PhD
on modular functions at the Free University of Amsterdam in 1943. From
1939 to 1944 N.G. de Bruijn was a full-time assistant at the Technical
University of Delft. That period helped him get through a large part
of the war without forced labour in Germany (Delft was in the hands of
the German during the war). De Bruijn started his professional career
as a researcher at the Philips Research Laboratory in Eindhoven from
1944 to 1946, then occupied a full professorship at the University of
Delft from 1946 until 1952 when he moved to a professorship at the
University of Amsterdam. In 1960, N.G. de Bruijn returned to Eindhoven
University as a professor of Mathematics at Eindhoven University of
Technology. De Bruijn's's contributions in the fields of Mathematics
and Computer Science are numerous. His book on advanced asymptotic
methods, North-Holland 1958, was a classic and was subsequently turned
into a book by the famous Dover books series as a result. His work on
combinatorics resulted in influential notions and results of which we
mention the de Bruijn-sequences of 1946 and the de Bruijn-Erdos
theorem of 1948. De Bruijn's famous contributions to mathematics
include his work on generalized function theory, analytic number
theory, optimal control, quasicrystals, the mathematical analysis of
games and much more. In each area he approached, he shed a new light
and was known for his originality. De Bruijn could rightly assume the
motto "I did it my way" as his own motto. And when it came to
automating Mathematics, he again did it his way and introduced the
highly influential Automath. In the past decade he has been also
working on the theories of the human brain.
Due to the varieties of contributions of de Bruijn, the workshop
concentrated on the computational aspects of Mathematics.
We are delighted to have had three exceptional invited speakers at the
workshop: Peter Aczel, Henk Barendregt and Rob Nederpelt, and are
sorry that just before the workshop, Robert Constable (also an invited
speaker) had an accident which meant he could not attend. The
abstracts of the invited talks are as follows:
Variable Binding and Logical Frameworks
Peter Aczel
These are two topics to which de Bruijn has made major contributions.
His contribution to the first topic was the today classic idea of `de
Bruijn indices' as a technique to use in the computer implementation
of variable binding operators. In recent years a variety of
mathematical treatments of variable binding have been proposed and
investigated. In the first part of my talk I will discuss the notion
of a nested data type and its use in representing variable binding.
De Bruijn may be said to be the inventor of the idea of a logical
framework in connection with his automath project. Today there are a
variety of logical frameworks that have been proposed, often differing
subtly by the features that they support. In the second part of my
talk I will report on the ideas and results, of the PhD student Robin
Adams, for classifying and comparing logical frameworks by the
features that they support. In general adding a new feature to a
logical framework often leads to a conservative extension.
Computations via proofs
Henk Barendregt
"Proofs via computations" by now is an established method within
Computer Mathematics. The converse, computations via proofs, has as
aim to use a (constructive or classical) proof as an algorithm,
whenever possible. Both theoretical and practical aspects will be
presented. Recent work of Cruz-Filippe and Spitters shows that there
is space for improvements in efficiency.
Recent Results in Type Theory and Their Relationship to Automath
Bob Constable
The notion of a telescope is basic to
Automath's theory structure; telescopes provide the context for
theorems. A dependent record type is an
internal version of a telescope and is used in Nuprl to define
theories. This paper shows how A. Kopylov defines these record types
in terms of dependent intersections, a
new type constructor.
Definitional equality and book equality are fundamental concepts basic to
Automath. In computational type theories these concepts appear in a
different form, as computational equalities and as quotient types.
Questions about these concepts
have led to interesting discoveries about types and open
problems. This paper presents a new formulation of quotient types by
A. Nogin, and an open question about them.
De Bruijn's language of Mathematics and weak type theory
Rob Nederpelt
De Bruijn intended Automath not just as a technical system for the
verification of mathematical texts, but rather as a life style with
its attitudes towards understanding, developing and teaching
mathematics. He believed that the way mathematical material is to be
presented to the system should correspond to the usual way we write
mathematics. In this talk, we discuss de Bruijn's philosophy of a
language of mathematics and the development of weak type theory.
In addition to the invited talks, there was a call for papers.
The papers in this volume were reviewed by the program committee
consisting, besides the editors, of
| Thierry Coquand | (Gothenburgh,
Sweden) |
| Jean-Louis Krivine | (Paris,
France) |
| Michael
Kohlhase | (Carnegie-Mellon, USA) |
| Rob
Nederpelt | (Eindhoven the Netherlands) |