cdk@dit.upm.es (Carlos Delgado Kloos) (03/25/89)
Workshop on Computer-aided Development of
Proofs, Theories, Programs, and Circuits
Madrid, 3-7 July 1989
Objectives
----------
The importance of computer support to formal methods for the development of
programs and mathematical theories is being recognised by an evergrowing
number of computer scientists, mathematicians, and philosophers. The goal of
this workshop is to fulfill some of the needs created by this interest. This
goal shall be achieved in two ways. First, by introducing interested people
into the field with tutorials, showing how one can develop interactively
mathematical theories, correct software, and even hardware. Second, having a
forum for the exchange of ideas and approaches for people working in this area
with the presentation of communications about their work.
Activities
----------
* Introductory Lecture by Prof. Martin Davis
(Courant Institute, New York University, USA)
Prof. Davis has had a great influence on the development of computability
theory and automatic theorem proving. His publications have confirmed him
as a great exposer of these subjects.
* Tutorial on HOL by Dr. Thomas Forster
(Cambridge University, United Kingdom) (10 hours, 2 hours/day)
HOL (Higher Order Logic) has been developed at Cambridge as a successor of
LCF (Logic for Computable Functions). It is mainly used to prove digital
circuits correct. Dr. Forster has used HOL to design a theorem prover.
* Tutorial on MIZAR by Prof. Andrzej Trybulec
(University of Warsaw, Branch of Bia\lystok) (10 hours, 2 hours/day)
MIZAR is a family of systems devoted to check the correctness of mathematical
proofs. Prof. Trybulec is the author and main designer of MIZAR.
* Communications (of 30 minutes) of participants on the following topics:
- Computational Logic
- Interactive Provers
- Proof Editors
- Transformational Programming
- Computer-aided Teaching of Logic
- LCF and HOL systems
- MIZAR systems
- Inference checkers
- Logical Obviousness
- Implementation of checkers
This list is not meant to be exhaustive.
Registration
------------
For the presentation of communications, two copies of an abstract (in Spanish
or English) of no more than 3 double-spaced pages are expected to be received
before 31 May 1989 at one of the addresses below.
During the tutorials, the participants will have the opportunity to practice
at computer terminals. For this reason, the number of participants in the
tutorials is restricted to 20 persons.
The registration fee is 20.000 pts, if received before 15 June 1989, and
30.000 pts after this date. Members of the Asociaci'on Espa'nola de
Inform'atica y Autom'atica and/or the IEEE will get a discount of 15%.
Payment is through Fundaci'on Universidad-Empresa with the attached form.
Organization
------------
The workshop is sponsored by the Asociaci'on Espa'nola de Inform'atica y
Autom'atica and the Spanish Chapter of the Computer Society of the IEEE and
jointly organized by the Departamento de Inform'atica y Autom'atica,
Universidad Complutense de Madrid, and the Departamento de Ingenier'ia de
Sistemas Telem'aticos, Universidad Polit'ecnica de Madrid, in cooperation with
Fundaci'on Universidad-Empresa.
For sending abstracts of communications, reserving accommodation at the
Colegio Mayor Loyola (Paseo Juan XXIII, 17, 28040 Madrid, approx. 2500
pts), or any question about the workshop, please contact:
Dr. Javier Leach
Depto. Inform'atica y Autom'atica
Facultad de Matem'aticas
Univ. Complutense de Madrid
E-28040 Madrid
Tel.: (+34-1) 4490174
E-mail: w039@emducm11.earn}
Dr. Carlos Delgado Kloos
Depto. Ing. Sist. Telem'aticos
ETSI Telecomunicaci'on
Univ. Polit'ecnica de Madrid
E-28040 Madrid
Tel.: (+34-1) 5495762 ext. 360
E-mail: cdelgado@dit.upm.es
Fax: (+34-1) 2432077
-----------------------------------cut here----------------------------------
Workshop on Computer-aided Development
of Proofs, Theories, Programs, and Circuits
Madrid, 3-7 July 1989
Registration form
Name: ....................................................................
Institution: .............................................................
Address: .................................................................
..........................................................................
..........................................................................
I want to attend the workshop and send ..................... pesetas
o by enclosing a cheque, or
o by bank draft
to the order of "Fundaci'on Universidad-Empresa", Ref: Workshop July 89,
Account No.19802/90, Banco Central, Oficina principal, Alcal'a 49,
28014 Madrid, Spain.
Send this form to: SICUEMA, Fundaci'on Universidad-Empresa, Serrano
Jover, 5 - 7a planta, 28015 Madrid, Spain, Tel.: (+34-1) 2419600