Subj:	Second Announcement
Date:    Fri, 1 May 1992 11:41:17 -0300 (ADT)
From: jfunk@kean.ucs.mun.ca

Atlantic Canada Algebra Conference

Sir Wilfred Grenfell College
Memorial University  of Newfoundland
Corner Brook, Newfoundland

Friday, Saturday and Sunday, May 22, 23, 24, 1992

The Mathematics Department of Grenfell College is pleased to
announce its first algebra and category theory conference.
The conference will coincide with an interdisciplinary
conference on Myth and Knowledge.  John Casti, author of 
"Paradigms Lost", will be speaking Saturday morning at 9:00.

There will be four sessions of talks on the mornings and afternoons of
Saturday and Sunday with the possibility for more talks on Monday.
On Friday evening, May 22, there will be a reception at the college.

Accommodations can be obtained from the following:

1. The Glynmill Inn
   Telephone: 1-800-563-4400 (Atlantic Provinces)
              (709) 634-5181 (Other)

2. College Residence
   Telephone: (709) 637-6321
   Room with shared bath: $29.40 (Cdn.) tax included.

If you would like to give a talk at the conference, or
would just like to attend, please notify one of the organizers
as soon as possible.

Organizers:

Jonathon Funk     (709) 637-6284 (office)
                        634-1934 (home)

Richard Macleod   (709) 637-6284 (office)
                        634-0545 (home)

Richard Squire    (709) 637-6290 (office)
                        639-1263 (home)               

_________________________________________________________________

Dept. of Mathematics and Statistics
Sir Wilfred Grenfell College
Corner Brook, Newfoundland
Fax: (709) 639-8125 (General Office)
==================================================================
Subj:	Oktoberfest
Date:    Tue, 12 May 1992 10:16:02 -0300 (ADT)
From: barr@triples.Math.McGill.CA (Michael Barr)

Fox has asked me to announce that there will be a Montreal meeting 
in October on the Thanksgiving/Columbus Day weekend.  I believe the dates
are Oct. 10 and 11.  More details will be forthcoming, but it will
be just like previous meetings.

Michael
==================================================================
Subj:	generalizations of monads and comonads
Date: Tue, 12 May 92 12:41:20 MET DST
From: Thomas Streicher <streiche@informatik.uni-muenchen.de>

During a discussion at the Durham meeting last year on monads versus  
comonads in semantics of programming languages Bill Lawvere made a  
remark on some recent work where a concept has been developed which  
generalizes both monads and comonads.
It should be the Thesis by a person called Thiebaud or Thibault or so  
...

I would be very grateful for any reference on this work !

Thomas Streicher
==================================================================
Subj:	A new book by Carl Gunter
Date:        Tue, 19 May 92 17:54:20 ADT
From: barr@triples.Math.McGill.CA (Michael Barr)

This just came from my account at Penn and I thought it was of interest.

From gunter@saul.cis.upenn.edu Mon May 18 17:41:36 1992
Date: Mon, 18 May 92 17:41:21 -0400
From: gunter@saul.cis.upenn.edu
Posted-Date: Mon, 18 May 92 17:41:21 -0400
Message-Id: <9205182141.AA05056@monroe.cis.upenn.edu>
To: lcs@saul.cis.upenn.edu
Subject: Draft 5 of book
Status: R


Draft 5 of my forthcoming book for MIT press is now (finally)
complete.  I'm having a copy made to put in the theory lab if you'd
like to have a look.  After writing the index, incorporating more
corrections, and adding a few more exercises, the final version will
be delivered to the press in mid-June.  The books themselves are
expected to be in bookstores by September.

I need some help with technical review of Chapters 9 and 11---the new
chapters on polymorphism.  If you have an interest in polymorphism and
a keen eye for detail, then I would very much appreciate your
assistance on proof-reading.  Send me email if you are willing to lend
a hand.

Here is a copy of the table of contents:


SEMANTICS OF PROGRAMMING LANGUAGES
Structures and Techniques

List of Tables
List of Figures
Series Foreword
Preface

1. Introduction					1
 1.1 Semantics
 1.2 Semantics of Programming Languages
 1.3 Notes

2. The Simply-Typed Lambda-Calculus		31
 2.1 Syntax of Lambda-Terms
 2.2 Rules
 2.3 Models
 2.4 Notes

3. Categorical Models of Simple Types		63
 3.1 Products and Cartesian Closure
 3.2 Lambda-Calculus with Constants
     and Products
 3.3 The Use of Category Theory
 3.4 Notes

4. Recursive Definitions of Functions		95
 4.1 A Programming Language for
      Computable Functions
 4.2 Fixed Points in Complete Partial Orders
 4.3 Fixed-Point Semantics of PCF
 4.4 Bounded Recursion
 4.5 Notes

5. Two Theories of Finite Approximation		141
 5.1 Bc-domains
 5.2 Stable functions and dI-domains
 5.3 Equivalences between categories.
 5.4 Notes

6. Relating Interpretations			169
 6.1 Full Abstraction
 6.2 Extensions of Adequacy Results
 6.3 Products and Sums
 6.4 Notes

7. Types and Evaluation				207
 7.1 Expressiveness
 7.2 Security
 7.3 Reference types
 7.4 Recursive Types
 7.5 ML Polymorphism and Type Inference
 7.6 Notes

8. Universal Domains				245
 8.1 Untyped lambda-Calculus
 8.2 Domain Equations
 8.3 Notes

9. Subtype Polymorphism				273
 9.1 Subtypes as Subsets
 9.2 Subsumption as Implicit Coercion
 9.3 Notes

10. Domain Theory				303
 10.1 Fixed Points of Functors
 10.2 Bifinite domains
 10.3 Adjunctions and Powerdomains
 10.5 Notes

11. Parametric Polymorphism			343
 11.1 Calculi for Expressing Parametric
      Polymorphism
 11.2 Indexed Families of Domains
 11.3 Notes

List of Notations				377
Bibliography					381
Subject Index					391

Subj:	Some abstracts from Barwise
Date:        Mon, 18 May 92 17:03:23 ADT
From: barr@triples.Math.McGill.CA (Michael Barr)

The attached abstracts, especially the last two, seem very interesting.

Michael

From chris@central.cis.upenn.edu Mon May 18 15:44:45 1992
Posted-Date: Mon, 18 May 92 15:39:52 -0400
Message-Id: <9205181939.AA15281@central.cis.upenn.edu>
To: missing-linc@linc.cis.upenn.edu, sloan-local@linc.cis.upenn.edu
Subject: Talks by John Barwise, May 19, 20, 21, 1992
Date: Mon, 18 May 92 15:39:52 -0400
From: Chris Sandy <chris@central.cis.upenn.edu>
Status: R

              Institute for Research in Cognitive Science
                     University of Pennsylvania
                         401C seminar room
                     3401 Walnut St., suite 400C

May 19, 1992            Talk No. 1: Channels           1:00 pm

A central debate in cognitive science and modern philosophy is
whether or not it is possible to give a naturalistic account of
intentionality.  How can we understand this ability of people and
other cognitive agents as part of the natural order, populating a
physical world governed by natural law?  Or must we understand the
physical world as a mental, linguistic, or social construct?

In this talk I want to propose a mathematical model for the notion of a
law-like regularity, which I will call a {\em channel}, into two parts:
a relationship between particular events (called a {\em signaling
relation}) and a relationship between types of events (called an {\it
indicating relation}).  The latter is a {\em regularity} by virtue of
reflecting properties of the former.  The two-level analysis allows us
to explain how regularities can be reliable but also admit of
exceptions, and allows us to unify a great many apprarently divergent
approaches to information and knowledge within a single framework.
The talk will be informal with the mathematics kept to a minimum.
Only at the very end will I point in the direction of connections with
the work of Freyd and Scedrov on the notion of an allegory.  Part of
this work is joint with Jerry Seligman.


May 20, 1992        Talk No. 2:  Logic and Diagrams         1:00 pm

When one looks at logic in practice, whether it be in science,
engineering, or everyday life, the extent to which various forms of
diagrammatic representation are used in design, reasoning, and problem
solving is more than striking; it is staggering.  Think about the
diagrams used in physics, chemistry, biology, hardware design, and
architecture, let alone geometry and topology.  But diagrams have been
largely ignored by logicians.  Aside from a few obvious
counter-examples (Euler, Venn, Frege, Peirce, e.g.), most logicians
have closed their eyes, and those of their students, to the
diagrammatic aspects of reasoning.  In this talk I will suggest that
logicians should study valid reasoning in systems of representation
that make use of such graphical devices as first-class
representations, and that they should teach principles of diagrammatic
reasoning to their students. I will go on to discuss some steps that
have been undertaken in that direction.  This talk is based on joint
work with John Etchemendy and a number of other people who will be
identified and blamed during the talk.

May 21, '92  Talk No.3: After the Revolution: Information and Academia  1pm

The function and structure of the research university (RU), as we have
come to know and love it, is based on certain assumptions.  I want to
examine some of these assumptions, suggesting that they are being
called into serious question by the information revolution.  If my
analysis is correct, the RU is in jeopardy and could go the way of the
the dinosaur, the ship-building industry in the 19th century, and the
Soviet Union.  I then want to propose some short-term measures
which should be taken to help RUs adapt, rather than succumb, to the
revolution.  This is not an area in which I am an expert, but it is
one where I have had many painful experiences, ones which give
rise to the reflections in the talk.





==================================================================
Subj:	informations
Date: Fri, 22 May 92 18:48:28 +0200
From: momathie@mathp7.jussieu.fr (Monique Mathieu)

Journees de travail  "ESQUISSES ET TYPES DE STRUCTURE"
organisees les  2 , 3 et 4Juillet 1992 a l'Universite Paris7
 et a l'Ecole Centrale de Paris sur le theme :
SYSTEMES, STRUCTURES, BASES DE DONNEES:
modelisations diagrammatiques et applications
(calcul formel,optimisation, theorie de la
demonstration, ....)
CONTACTER : L. Coppey ou M. Mathieu
UNIVERSITE PARIS 7    U.F.R. de Mathematiques
Tours  45-55,  5eme etage
2 place  JUSSIEU
75251 PARIS CEDEX 05
FRANCE
e-mail: coppey@mathp7.jussieu.fr
    ou  : momathie@mathp7.jussieu.fr
==================================================================
Subj:	modified realizability and intensional type theory
Date: Mon, 25 May 92 18:23:50 MET DST
From: Thomas Streicher <streiche@informatik.uni-muenchen.de>

TRULY INTENSIONAL MODELS OF TYPE THEORY
ARISING FROM MODIFIED REALIZABILITY


The definition of what is a model structure for intensional  
Martin-Loef Type Theory has been given by John Cartmell  in his  
Thesis (Oxford 1978). Essentially it is like semantics for  
extensional type theory with the only exception that one drops  
uniqueness constraints and replaces them by the constraint that  
Eliminators are preserved by substitution.

There has been described quite a lot of models for extensional type  
theory mainly based on the idea of Kleene realizability. The most  
important structure in this context is the category of so called  
realizability sets which we will refer to by  r-Set and the full  
reflective internally complete subcategory PER.
It seems to be impossible to find truly intensional models for type  
theory in this setting as extensionality is built in almost by  
definition. (Extensionality for me means that the terminal object is  
a generator).

But instead of considering a category of Kleene realizability sets  
one can also build a category based on KreiselBs Modified  
Realizability. Whereas in Kleene realizability propositions are  
considered as arbitrary sets of natural numbers the key idea of  
modified realizability is to endow any such set  A  of natural  
numbers with a subset  B . The set  A  has to be thought of as the  
collection of potential realizers and the subset  B  as the  
collection of ACTUAL REALIZERS.

This intuitive idea can be lifted to realizability sets. Based on the  
category  r-Set  of realizability sets  we construct a category   
mr-Set  of so called  "modified realizability sets".


Description of  mr-Set  :

objects :     triples   ( X , d(X) , r(X) )  such that 


                  (1)  X  is a set
			  

		  (2)  d(X)  is a subset of  X 


                       (objects in  d(X)  will be called "defined")
				
		  (3)  ( X , r(X) )  is an r-set , i.e.
				
		         r(X)  is a relation between natural numbers      

                         and  X  such that for any  x  in  X  there
                         is a natural number  n  with  n r(X) x
					
					
morphisms :     a morphism from   ( X , d(X) , r(X) )   


                             to   ( Y , d(Y) , r(Y) )

                is a set-theoretic function   f : X -> Y  such that
			    

	
        (1)     f (x)  is in  d(Y)  provided that   x  is in  d(X)
			   

	        (i.e.  f  preserves actual realizers !)
				      

			   

        (2)     f  is a morphism from  ( X , r(X) )  to  ( Y , r(Y) ) 

                in  r-Set
			   

			   

	        ( i.e.  there is a natural number  n  such that for
                  all  x  in  X  and  m  with   m r(X) x  :  

                

                      {n}(m)  is defined and  {n}(m) r(Y) f(x)    ) .
								 
				 

More abstractly the category  mr-Set  can be described as the result  
of the Grothendieck construction applied to the fibration of REGULAR  
MONOs in  r-Set  over  r-Set .

The category r-Set  is a full reflective subcategory of  mr-Set  by  
the embedding sending 



        ( X , r(X) )    to     ( X , X , r(X) )    .


THEOREM   Just as r-Set  is locally cartesian closed so is  mr-Set.

          The category mr-Set  is not extensional.

Proof :  Obviously,  mr-Set  has finite limits.

         The Pi-s  are computed as in r-Set ,  BUT elements are  

          defined iff they preserve definedness.
	      

	  The underlying r-set of the terminal object in  mr-Set  is
          the terminal object in  r-Set and all elements are defined.
	  Of course, there exist two different parallel morphisms in 

          mr-Set  which coincide on defined elements and such 

          morphisms cannot be separated by global elements, i.e.
          morphism whose source is the terminal object.	

	      

As  mr-Set is left exact it constitutes a model of extensional type  
theory.

Nevertheless we can interpret intensional identity typs in a way such  
that they do not fulfill the laes of extensional identity types.

For this purpose we consider  mr-Set  as a model of the ambient  
logical framework.

For what Martin-Loef calls "constructive set theory" we have to  
identify a certain full subcategory  of  mr-Set.


DEFINITION    A small set is an object  ( X , d(X) , r(X) )  in 

              mr-Set  such that

      (1)    n   r(X)  x1  and   n   r(X)  x2    implies    x1 =  x2
			 

      (2)    for some object   x   in  X  we have    0 r(X)  x  .
			    

	
In the sequel we shall need two distinguished small sets :


   Succeed  =  ( {e , r} , {r} ,  { ( 0 , e ) , (1 , r ) })    and
  

   Fail    =   ( {e} , {} ,  { (0,e) } )      .
			    


Now we shall interpret Martin-Loefs identity types in  mr-Set  in  
such a way that they do not satisfy the laws of extensional identity  
types.
			  

If  A  is a small set and  a1 ,  a2  are objects of the underlying  
set of  A  then

      

     Id A a1 a2  =  Fail          if  a1  and  a2  are different
			
     Id A a a  =  Succeed   .
		      

		      

For any small set   A   and  a  in  A  (not necessarily defined!)   



                          r A a  =  r      .
			 

			 

Finally we give the definition of the elimination operator  J .

Given   A : Set   and  a family

        C : {a1 , a2 : A} {c : Id A a1 a2} Set   and a function

        d : {a : A}  C a a (r A a)
			
			
the function


        J A C d   :    {a1 , a2 : A} {c : Id A a1 a2}  C a1 a2 c
			  

			  

is defined as follows


              J A C d a a r  =  d a
				    

	      J A C d a1 a2 e  =  the unique object in  C a1 a2 e 

                                      realized  by  0               .
				
				
Obviously,  J  is realizable as one simply performs a decidable case  
analysis on the realizer for the lasr argument.


THEOREM     The following  sequents are NOT valid in this model   :

 

(1)      A : Set , x : A  ,  y : A  ,  z  : Id A x y  |-  x = y : A
	
	
	      [ but, of course, theer is a term   t   such that
			
			
		  A : Set , x : A  ,  y : A  ,  z  : Id A x y 


                  |-  t  :  Id Ax y : A                           ]

	
(2)       A : Set ,  C : A -> Set , x : A  ,  y : A  ,  z  : Id A x y 


          |-  C x = C y
	
	
	     [ put  for  A  a small set 

               with at least two different 

               objects  a   and  b
	       where  a  is assumed to be defined  

	       and for  C  the family  [x:A]  Id A a x  ;
		     

               then we have    Id A a a   =  Succeed     


                        but    Id A a b  =  Fail
			   

			although   e : Id A a b              ] .
			  

			  

			  

(3)      The socalled  Equality Reflection Lemma
         (terminology of LuoBs Thesis) holds
	


         If  |-  p : Id A t s    is valid in the model       

			
         then      |-  t = s : A    is valid in the model, too.
			
			
(The restriction to the empty context is important, see (1) ! The  
interpretation of the empty context contains one defined and no  
undefined object ! ).
			
			
			
THEOREM    


In the model defined above the principle of extensionality


  {A,B : Set} {f,g : A->B} ({x:A} Id B (f x) (g x)) ->  Id (A->B) f g
			      

			    

is NOT realized !!
			    


 Proof :  by a continuity argument !!
			
			
			
			
			
//**  In General Leibniz Equality is different from Martin-Loef  
Idenity Types  **//


Interpret   Prop   as small sets and interpret  Type(0)  as those   
mr-sets  where the underlying r-set is a per. 


Then both  Prop  and  Type(0)  are closed under arbitrary internal  
products.

In  Type(0)  we can interpret (even extensional)  Martin-Loef  
identity types as we have mr-sets whose underlying  r-set  is empty.

On the other hand we can define Leibniz equality employing  Prop .


Now let   A  be a type containing ar least two different defined  
elements  a1  and  a2 .

Then    LE A a1 a2   is in  Prop  containing no defined element BUT  
surely a nondefined element realized by  0  .

Id A a1 a2  contains not even an undefined element.

Therefore there cannot exist a morphism from   LE A a1 a2    to    Id  
A a1 a2   !!



Thomas Streicher
