mcvax!dipisa!longo | 18 Sep 17:22 1988

Professorships in Italy

Date: Wed, 14 Sep 88 17:30:36 MET


18 (eighteen) positions as full professor are available in 11 different
Universities in Italy, in Computer Science.  
There is no nationality nor language limitation (the last time 10 or 12
foreigners, from USA, Turkey, Poland, West Germany... obtained 
these positions in Computer Science and Mathematics).
The competition is handled nationally by a commettee which will be 
appointed by the Ministry of Education and is only based on Curricula
Vitae (resumes). 
Anybody interested may ask for a copy of the forms and directions to
Giuseppe Longo (tel. --39-50-510244; or Stefania --39-50-510111). In 
order to complete the application one may need some help by an italian 
speaking person (the signature of a notary, certifying the identity
of the candidate, must be notarized (!) at an italian Consulate). 
    The deadline is NOVEMBER 5.
As bureaucracy is slow, the procedure may take a couple of years, or
more, before one can actually start working.
Please do apply, if you feel qualified.  Italy is a rather beautiful
country and, in some places, there is also some good Computer Science
(and, once in the University State system it is rather easy to move
>from a University to another).
Good luck.

gray | 20 Sep 01:54 1988

Mitchell's problem

Date: Mon, 19 Sep 88 16:32:15 CDT

I tried to post this note earlier and failed, so I'll try
	"Problem for domain theorists: what is the smallest 
category containing your favorite domains (Scott domains, L-domains,
whatever you like) and closed under pullbacks?"

	I would like to amplify on Andy Pitt's response to John
Mitchell's query.  The theory of sketches treats exactly this kind of 
question.  (See, Barr and Well, Toposes, Theories and Triples,
Springer-Verlag,  or my paper, Categorical Aspects of Data Type
Constructors, TCS 50, 103-135.)  Sketches are presentations of
equational Horn theories (actually a bit more).  There is a sketch,
S1, for categories with finite products, in the sense that the 
category of models of this sketch is the category of small categories
with chosen finite products..  There is another sketch, S2, for 
categories with finite products and pullbacks and an
inclusion sketch homomorphisms: S1 -> S2. It induces a "forgetful" 
functor, the other way on categories of models; U: MOD(S2) -> MOD(S1).

	John's question can be interpreted as asking for information 
about the left adjoint functor going the other way:
	h* : MOD(S1) -> MOD(S2),
whose value on a small category C with finite products is the free
category h*(C) with finite products and pullbacks.  The general
theory of sketches guarantees that this left adjoint functor exists,
but it doesn't give very much information about it.  For instance,
consider the adjunction morphism (which in this case is a functor),
	eta : C -> U h*(C).
(Continue reading)

Val Breazu-Tannen | 1 Oct 01:32 1988

inheritance, coercions and polymorphism

Return-Path: <val@...>
Date: Thu, 22 Sep 88 10:58:34 EDT
Posted-Date: Thu, 22 Sep 88 10:58:34 EDT
Cc: gunter@..., andre <at>

>FROM   Val Breazu-Tannen, Carl Gunter and Andre Scedrov
               University of Pennsylvania

This is a short announcement about our progress on providing a model
for FUN (see Cardelli & Wegner, Computing Surveys, 17 (1985), pp.
471--522) extended with full recursive types. (Recently, Bruce &
Longo, as well as Martini, have provided models for FUN, but without
recursive types.) We have not yet written out full details for
variants and existential quantifiers, but we hope to get to these in
due course; the rest of the language (and, of course, recursive types)
seems to work out satisfactorily with our approach.

Say FUNREC is FUN (C. & W. pp. 519--520) without existentials and
variants, but with full recursive types.

Our technique is based on the idea that expressions from FUNREC can be
translated into expressions in the polymorphic lambda calculus with
records and recursive types (which we'll call "enriched F2" below).
More precisely, a derivation of an inheritance judgement or typing
judgement in FUNREC is translated into a derivation of a typing
judgement in enriched F2. In particular, bounded universal
quantification is translated as follows:

      T[ForAll a<r. s] = ForAll a. (a -> T[r]) -> T[s]

(Continue reading)

meyer | 1 Oct 01:43 1988

talk at MIT: Curtis `Strong Typing in Scheme', 10/4/88

			   Strong Typing in Scheme

				Pavel Curtis
			 Computer Science Laboratory
				 Xerox PARC

	    Tues, Oct 4, 2:30pm (refreshments at 2:00, probably)
		      545 Technology Square, Room 512A

Abstract: Compile-time checking of data type usage in programs has
long been recognized as a helpful tool for discovering and preventing
bugs in programs.  Some have even claimed that such static type
analysis (called ``strong typing'') is a prime enabler of the
construction of robust large software systems.  Previously-known
techniques for strong typing, however, have allowed only very strict
and inflexible type systems to be built, such as those of Pascal and
ML.  Mixing the advantages of strong typing with the great flexibility
and expressive power of languages like Scheme has not yet appeared
possible.  Recent work, however, appears to have made great strides
toward this goal.  We have thus been inspired to begin serious work on
a practical system for strong typing in Scheme.  We believe that the
facilities in our current system will prove sufficient to account for
the type safety of most existing Scheme code, including programs that
make significant use of polymorphism, side-effects, continuations, and
higher-order procedures.  This talk will cover the major points of our
system and the current status of the work in progress.

Mitchell Wand | 1 Oct 01:46 1988

Upcoming Schedule

Date: Thu, 29 Sep 88 10:28:16 EDT
To: lieber@..., abbas <at>,
        zywang@..., woolf <at>,
        oliva@..., holland <at>,
        riel@..., bwhite <at>, gerald <at>,
        muller@..., kfoury <at>, raf <at>,
        snyder@..., trung <at>, dsmith <at>,
        jmiller@..., mairson <at>,
        pmo%icad.uucp@..., attend-types <at> theory.LCS.MIT.EDU,

The Semantics Seminar will meet on Wednesdays from 9:00 to 11:00 in Room 107
Cullinane at Northeastern.  All are invited to attend.

10/5	Mitch Wand	Type Inference for Multiple Inheritance
10/12	Bill White	Curien: The Categorical Abstract Machine

Coming attraction:
	Wayne Snyder	Higher-Order Unification

John Mitchell | 1 Oct 02:14 1988

type theory and practice

Date: Thu, 29 Sep 88 14:56:42 PDT

Earlier this week, Luca Cardelli and I gave a half-day
tutorial on "semantic methods for object-oriented
languages" at the ACM OOPSLA (Object-Oriented Programming:
Systems, Languages and Architectures) Conference.
Since our presentation was far more "theoretical" than
anything else at past or present OOPSLA's, we expected
around 30-50 attendees. Instead, the tutorial sold out,
with 210 people paying $100 each. (Too bad we didn't
get a percentage.) We had comments from database 
designers at small companies like, "all of the 
issues you discussed here were problems we had to
confront in designing our object-oriented database
product." So I think type theory is having a significant
impact on computing practice.

(Incidently, the tutorial which was based on our past 
work on types and objects. Specifically, we handed out
Luca's paper in Computing Surveys with Peter Wegner, 
and my paper with Lalita Jategaonkar
>from this year's ACM Lisp and FP conference.)

John Mitchell

John Mitchell | 1 Oct 02:16 1988

new course at Stanford

Date: Thu, 29 Sep 88 17:23:37 PDT

Here is a tentative outline for a course I am teaching this
fall. I would be interested in comments, suggestions, and
outlines of similar courses taught elsewhere.


                       CS 258
         Introduction to Programming Language Theory
                     Fall 1988

                  John Mitchell
               Stanford University

Course Outline

1. Introduction
	a. Overview of course
	b. The simple programming language PCF
	(typed lambda calculus with functions, pairs,
	integers, booleans and recursion)
2. Typed lambda calculus
	a. Context-sensitive syntax 
	b. Equations, proofs, and reduction rules
	c. Semantics, and soundness of the proof system
	d. Three examples of semantic models
	(set-theoretic, recursion-theoretic and 
(Continue reading)