Editorial
Herman Geuvers and Fairouz Kamareddine
Simple canonical representation of rational numbers
Yves Bertot
Eigenvariables, bracketing and the decidability of
positive minimal intuitionistic logic
Gilles Dowek and Ying Jiang
Automath and Pure Type Systems
Fairouz Kamareddine, Twan Laan and Rob Nederpelt
Tactics and parameters
Gueorgui Jojgov
On the structure of Mizar types
Grzegorz Bancerek
Explicit substitutions à la de Bruijn: the local and global way
Fairouz Kamareddine and Alejandro Rios
Remarks on isomorphisms of simple inductive types
David Chemouil and Sergei Soloviev
Polymorphic type checking for the ramified theory of types of Principia Mathematica
Randall Holmes
Editorial
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) |
The eight accepted papers have all been influenced in one way or another by the work of de Bruijn and his influence will continue for years to come.
We wish N.G. de Bruijn a long and healthy life and long live his powerful influence in our field.
This volume has been published as volume 85.7 in the series Electronic Notes in Theoretical Computer Science (ENTCS). This series is published electronically through the facilities of Elsevier B.V. and its auspices. The volumes in the ENTCS series can be accessed at the URL
We are grateful for the excellent help and support received from the ICALP2003 chair Jos Baeten, the workshop coordinator Erik de Vink, and the organisers Tijn Borghuis and Anne-Meta Oversteegen.
July4-5, 2003 | Herman Geuvers and Fairouz Kamareddine |
© Copyright 2003, Elsevier Science, All rights reserved.