Archives

Please note that this newsitem has been archived, and may contain outdated information or links.

12 November 2004, VvL symposium "Logica in de Lage Landen", Room 414, Jaarbeurs, Utrecht

Date: Friday 12 November 2004
Location: Room 414, Jaarbeurs, Utrecht

(dutch only)
De Vereniging voor Logica en Wijsbegeerte der Exacte Wetenschappen (VvL) nodigt u hierbij uit voor een VvL symposium "Logica in de Lage Landen". Deze gebeurtenis vindt plaats op vrijdag 12 november 2004 in zaal 414 van de de Jaarbeurs in Utrecht. Het programma begint om 12.45 met een broodjeslunch, u aangeboden door de VvL, tijdens de jaarlijkse Algemene Ledenvergadering.

Alle belangstellenden zijn van harte welkom. De toegang is gratis. Abstracts van de lezingen vindt u onderaan.

Met vriendelijke groet,
Rineke Verbrugge, secretaris

Programma:



[12.45-13.30] Broodjeslunch annex VvL algemene ledenvergadering
[13.30-14.15] Dirk van Dalen, "Wat dacht Brouwer van de logica?"

[14.15-14.30] koffie- en theepauze
[14.30-15.15] Gerard Alberts, "Van Wijngaarden en logica: een gemiste verbinding"
[15.15-15.30] koffie- en theepauze
[15.30-16.15] Rob Nederpelt, "Automath"
[16.15-17.00] borrel

Abstracts


Dirk van Dalen: Wat dacht Brouwer van de logica?


Er zijn nauwelijks gegevens over Brouwers opvattingen waar het de logica betreft. In de correspondentie met Korteweg komen wat provocerende opinies voor, maar die kunnen niet als maatgevend beschouwd worden. De dissertatie geeft hier en daar wat commentaar op de logica, en verder kunnen we alleen afgaan op ``logica in gebruik". Niettemin is het lonend om nader op de schaarse gegevens in te gaan.

Gerard Alberts: Van Wijngaarden en logica, een gemiste verbinding


Vanaf het allereerste begin van computers is de verbinding gelegd tussen denken en computers (Von Neumann, Wiener, Turing). De achtergrond van mathematische logica bij het denken over berekenbaarheid (Post, Church, Turing) is door Martin Davis goed beschreven. Er wordt rond 1950 druk geconfereerd over rekenmachines als toegepaste logica (vanuit Nederland heeft Freudenthal zich daarmee bemoeid). Dat blijft allemaal bij abstracte speculaties, met de feitelijke bouw van rekenautomaten en programmeren heeft dat nog vrijwel niets te maken.
Serieus werd het in de jaren zestig toen men echt probeerde logica toe te passen op het ontwerp van programmeertalen en later op vraagstukken van programmacorrectheid.
Mijn bijdrage is gecentreerd rond Van Wijngaardens opstel ``Generalized Algol'' uit 1962 waarmee hij een schot voor de boeg gaf aan zijn collega's in het nadenken over een opvolger van ALGOL 60. Het gebeurde in Rome op de conferentie waar de basis werd gelegd voor WG 2.1, de IFIP-werkgroep waarbinnen Van Wijngaarden zijn belangrijkste invloed zou uitoefenen. De voordracht was wonderlijk omdat hij heel ver ging in de abstractie van het idee van programmeertaal. De voordracht was nog wonderlijker omdat hij duidelijk vroeg om logica (en noties van syntax en semantiek) en tegelijk liet zien dat Van Wijngaarden daarmee niet vertrouwd was: een gemiste verbinding.

Rob Nederpelt: Automath


Around 1967, the well-known Dutch mathematician N.G. de Bruijn developed a formal language for mathematics, which he baptized `Automath', since he wanted to Automate Mathematics. In the language Automath he included essential aspects of mathematics like definitions and proofs, which up to that day were mainly treated as being meta-mathematical. His aim was that the logical framework present in Automath would be strong enough not only for expressing mathematical content, but also for its (automatic) verification. For the latter purpose he wanted to call in the computer, which in that time only just had started its triumphal progress.
De Bruijn succeeded in designing a powerful and elegant formal language, suitable for his purposes. It was immediately implemented on a machine and tested with a large corpus of mathematical texts, taken from various fields and with complexity ranging from introductory to very advanced.
In the talk I first sketch the history of the Automath project. Next, I discuss some basic innovations first introduced in this formal language, in particular the well-organized (line-by-line) definitional structure and the influential `propositions-as-types' notion. Finally, I describe the connections of Automath with modern type systems such as the ones coined by Henk Barendregt.

Please note that this newsitem has been archived, and may contain outdated information or links.