CS.HAM@R20.UTEXAS.EDU (Hamilton Richards) (04/02/87)
Preliminary Announcement
The 1987 UT Year of Programming
with the support of the
U. S. Office of Naval Research
announces
The Institute on Logical Foundations of Functional Programming
Scientific Director: Dr. Gerard Huet, INRIA
Austin, Texas
8-12 June 1987
There is a growing realization that mathematical logic provides a foundation on
which programming languages and environments for software engineering can be
soundly based. Such a foundation should include a highly expressive notation
for formalisation of requirements, an efficiently implementable language for
coding programs, and a means of systematically deriving each program from its
specification, together with such proofs of correctness as are needed.
This Institute concentrates on a particularly simple paradigm. The type
verification rules of a programming language such as PASCAL or ADA may be
seen as a logical inference system. The rules of inference can be extended in
a uniform manner to check the validity of a program with respect to more
general formalized comments, assertions, and specifications. A powerful
constructive logic may thus be considered as the backbone of a pure, strongly
typed, functional programming language. We may thus envision programming
environments for such languages in which programs are designed consistently
with formal specifications. In such a system, a well-typed program serves as
its own proof of correctness, which may be checked by type-checking throughout
the period of program development. There is hope that in the future some of
the more routine parts of programs can be generated with machine assistance.
This approach to software engineering is currently the subject of much
speculation and research, involving both theory and practical implementation.
One of the leading research projects is Project Formel, which is jointly
sponsored by INRIA (Rocquencourt, France) and Ecole Normale Superieure (Paris)
and led by Dr. Gerard Huet of INRIA and Prof. Guy Cousineau of ENS. The Year
of Programming has invited Dr. Huet and his senior colleagues to present
their work in the Institute on the Foundations of Functional Programming.
The first three days of the Institute will be a tutorial on type theory,
functional programming, and their relationship to one another. It will prepare
students with some background in theoretical computer science for the more
advanced Research Seminar on Thursday and Friday, at which presentations will
be made of research in progress in several countries around the world.
The tutorial on functional programming and type theory will present a unified
view of computational structures described by categorical combinators. These
combinators may be seen as proof combinators from a sequent formulation of
intuitionistic logic, or alternatively as the building blocks of an
environment-manipulating machine well suited for executing lambda-calculus and
other functional programming languages. This introduces the Categorical
Abstract Machine (CAM) (a simplification of Landin's SECD machine) for
executing call-by-value lambda-calculus. The language CAML (Categorical
Abstract Machine Language) is closely derived from languages such as ML and
Hope. The compilation of CAML on the CAM will be discussed and compared with
related projects (ML on the FAM and the G-machine, Amber on the Amber machine).
Polymorphic types and the problems of type synthesis will be discussed at two
levels: ML's parametric polymorphism, and full polymorphism in Girard's
second-order lambda-calculus. A very general logical framework, the Calculus
of Constructions, will be described. It will be shown how this formalism
combines the expressive power of Girard's higher-order polymorphic
lambda-calculus, Martin-Lof's theory of types, and de Bruijn's AUTOMATH. The
tutorial will be taught by Prof. Cousineau and Dr. Huet, the scientific leaders
of Project Formel where CAM, CAML, and the Calculus of Constructions have
been designed and implemented. An implementation of CAML on SUN workstations
will be available for demonstrations and practical exercise sessions.
The Research Seminar will present research topics in Linear Logic and
Constructive Semantics. Linear Logic, a new formalism designed to serve as a
logical foundation for parallel programming, will be presented by its inventor,
Prof. Jean-Yves Girard, Groupe de Logique Mathematique, Universite Paris 7.
Under the general title of Constructive Semantics, recent research in Type
Theory under way at various centres in the USA and in Japan will be presented
by four research leaders in the field: Prof. Albert Meyer (MIT), Dr. John
Mitchell (AT&T Bell Laboratories), Dr. Susumu Hayashi (RIMS, Kyoto University),
and Prof. Andre Scedrov (U. of Pennsylvania). The Seminar program will be
augmented by short communications of research work in progress by the seminar
participants.
It is recommended that potential participants in the seminar register early.
In order to facilitate interaction, the number of participants will be limited.
Tentative schedule.
1. Tutorial on Functional Programming and Type Theory (June 8-10)
Monday.
8-10 Elements of category theory (GH)
10-12 Introduction to the ML language (GC)
2-4 A tutorial on lambda-calculus (GH)
4-5 Programming session: CAML
Tuesday.
8-10 Polymorphic type-checking (GC)
10-12 Natural deduction, the Propositions as Types principle (GH)
2-4 The Categorical Abstract Machine (GC)
4-5 Programming session: CAM
Wednesday.
8-10 The polymorphic lambda-calculus (GH)
10-12 Compiling functional languages; CAML Implementation (GC)
2-4 Type theory, the Calculus of Constructions (GH)
4-5 Programming session: Constructions
2. Research Seminar on Linear Logic and Constructive Semantics (June 11-12)
Thursday.
8-12 Qualitative domains, Coherent spaces. (J.Y. Girard)
2-330 Guest Lecture 1 (A. Meyer)
330-5 Guest Lecture 2 (J. Mitchell)
Friday.
8-12 Linear Logic. (J.Y. Girard)
2-330 Guest Lecture 3 (S. Hayashi)
330-5 Guest Lecture 4 (A. Scedrov)
Prerequisites: same as for graduate-level course in theoretical computer
science; programming experience is recommended.
Recommended readings:
G. Cousineau, P.L. Curien and B. Robinet, eds., Combinators and Functional
Programming Languages. Springer-Verlag, Lecture Notes in Computer Science 242,
1986.
L. Cardelli and P. Wegner. "On Understanding Types, Data abstraction, and
Polymorphism". ACM Computing Surveys 17, 4 (Dec. 1985): 471-522.
J. R. Hindley and J. P. Seldin. Introduction to combinatory logic and lambda
calculus. Cambridge University Press, 1986.
H. Abelson and G. J. Sussman. Structure and Interpretation of Computer
Programs. MIT Press 1985.
J. Lambek and P. J. Scott. Introduction to higher order categorical logic.
Cambridge University Press, 1986.
The U. T. Year of Programming
The Institute on Logical Foundations of Functional Programming is the third in
a series of Programming Institutes comprising the 1987 U. T. Year of
Programming, which is underwritten principally by the U.S. Office of Naval
Research, with supplementary funding from the University of Texas, Lockheed
Missiles and Space Company, and other sponsors. The other Institutes in the
series are:
Concurrent Programming (23 February - 6 March)
C.A.R. Hoare (Texas and Oxford)
Encapsulation, Modularization, and Reusability (1-10 April)
D. Gries (Cornell)
Formal Specification and Verification of Hardware (29 June - 3 July)
M.J.C. Gordon (Cambridge)
Declarative Programming (24-29 August ) D.A. Turner (Kent)
Specification and Design (14-25 September) J.R. Abrial (Paris)
Formal Development of Programs and Proofs (autumn) E.W. Dijkstra (Texas)
FOR FURTHER INFORMATION
To receive announcements and application forms for individual Programming
Institutes (this one or any of the others), please contact the Year of
Programming Office at one of the following addresses:
U. T. Year of Programming INTERNET: cs.ham@R20.UTEXAS.EDU
Department of Computer Sciences INTERNET: ham@SALLY.UTEXAS.EDU
Taylor Hall 2.124
The University of Texas at Austin telephone: 512-471-9526
Austin, Texas 78712-1188
-------