[Flirts] RE: Curry-Howard isomorphism for Institutions

[Joseph Goguen]

Dear Valeria,

It seems that Wadler and I agree with each other, and disagree with you,
in saying that programmers do not use CHI even though they do use types.

Also, there seems to be a bug in the Wadler paper, in that he proves that
the product type constructor is commutative (there are also a few smallish
exaggerated claims, but not this one).

Valeria.dePaiva at parc.com wrote:

>-----Original Message-----
>From: de Paiva, Valeria <Valeria.dePaiva at parc.com> 
>Sent: Monday, August 15, 2005 10:24 PM
>To: 'Joseph Goguen'
>Cc: 'flirts at informatik.uni-bremen.de'
>Subject: RE: [Flirts] RE: Curry-Howard isomorphism for Institutions
>
>Dear Joseph,
>
>I'm glad you've enjoyed Phil's paper. 
>  
>
>>My impression (e.g., looking at recent POPL proceedings) is that thereis indeed a lot of work that applies ideas from type theory to 
>>programming languages,  but the systems used are far from beautiful, 
>>while the beautiful systems are not directly useful.
>>    
>>
>
>My point was that the work represented in POPL, etc owes its existence to programmers picking up the CHI and using it for their own purposes.
>  
>
>Maybe it is  too much to  ask for  the systems that come from logic,  to
>carry-on being pretty. But I guess one may hope and I do. 
>I also enjoyed very much David Walker's invited talk at IMLA this year,
>when he was asking  the logicians in the audience for help with his type
>systems for memory management. But I guess there's no paper written
>about it, (yet, perhaps, I don't know). 
>
>I have written some of my own take on these ideas, as far as CHI for
>modal logics is concerned, in the preface of the special issue of the
>JLC dedicated to the second IMLA (2002 in Copenhagen). You can read it
>from http://www.cs.bham.ac.uk/%7Evdp/publications/final-preface.pdf
>if interested. But this is of course just a subcase of the general
>picture.
>
>Best,
>Valeria 
>  
>
i will take a look at your paper when i get a chance.

cheers,

joseph

>-----Original Message-----
>From: Joseph Goguen [mailto:goguen at cs.ucsd.edu]
>Sent: Monday, August 15, 2005 6:52 PM
>To: de Paiva, Valeria <Valeria.dePaiva at parc.com>
>Cc: flirts at informatik.uni-bremen.de
>Subject: Re: [Flirts] RE: Curry-Howard isomorphism for Institutions
>
>Dear Valeria,
>
>Thanks for the pointer to Phil's paper, i enjoyed reading it!
>
>This paper does not make the claims for Curry-Howard that you mention,
>but instead makes the much more modest claim that systems were "designed
>by researchers in functional languages and they depend heavily on logics
>and type systems whose roots were traced in this paper" (these roots are
>work of Church, Gentzen, Girard, etc.).  On the whole, there are
>pleasingly few exaggerated claims in the paper.
>
>My impression (e.g., looking at recent POPL proceedings) is that there
>is indeed a lot of work that applies ideas from type theory to
>programming languages, but the systems used are far from beautiful,
>while the beautiful systems are not directly useful.  It would be
>surprising to me if anyone worked out a Curry-Howard isomorphism for any of these ugly type systems.
>
>  - joseph
>
>Valeria.dePaiva at parc.com wrote:
>
>  
>
> _______________________________________________
>
>Flirts mailing list
>Flirts at mail.informatik.uni-bremen.de
>http://www.informatik.uni-bremen.de/mailman/listinfo/flirts
>  
>