This is not directly related to mizar, but since mizar's type system can cause so much pain and pleasure, the slides linked to in the forwarded message might be a fun diversion. Jesse
--- Begin Message ---
- To: types-announce-nHFbR+4dATOoZA3Q9b/B0PZ8FUJU4vz8@public.gmane.org
- Subject: Types Considered Harmful
- From: Benjamin Pierce <bcpierce-bBguPyWdlyqyum0STUha2w@public.gmane.org>
- Date: Fri, 4 Jul 2008 16:43:52 -0400
- Approved: news@gmane.org
- Archived-at: <http://permalink.gmane.org/gmane.comp.science.types.announce/800>
- Envelope-to: gcst-types-announce-Uylq5CNFT+jYtjvyW6yDsg@public.gmane.org
- List-archive: <http://lists.seas.upenn.edu/pipermail/types-announce>
- List-help: <mailto:types-announce-request-nHFbR+4dATOoZA3Q9b/B0PZ8FUJU4vz8@public.gmane.org?subject=help>
- List-id: Announcements of interest to the TYPES community <types-announce.lists.seas.upenn.edu>
- List-post: <mailto:types-announce-nHFbR+4dATOoZA3Q9b/B0PZ8FUJU4vz8@public.gmane.org>
- List-subscribe: <http://lists.seas.upenn.edu/mailman/listinfo/types-announce>, <mailto:types-announce-request-nHFbR+4dATOoZA3Q9b/B0PZ8FUJU4vz8@public.gmane.org?subject=subscribe>
- List-unsubscribe: <http://lists.seas.upenn.edu/mailman/listinfo/types-announce>, <mailto:types-announce-request-nHFbR+4dATOoZA3Q9b/B0PZ8FUJU4vz8@public.gmane.org?subject=unsubscribe>
- Newsgroups: gmane.comp.science.types.announce
- Original-received: from rhizome.seas.upenn.edu ([158.130.69.24]) by lo.gmane.org with esmtp (Exim 4.50) id 1KFr8H-0000Vx-5d; Mon, 07 Jul 2008 15:51:57 +0200
- Original-received: from RHIZOME.SEAS.UPENN.EDU (LOCALHOST.upenn.edu [127.0.0.1]) by rhizome.seas.upenn.edu (8.13.6/8.12.8) with ESMTP id m67Dk8X5021362; Mon, 7 Jul 2008 09:46:09 -0400
- Original-received: from psychopathy.seas.upenn.edu (psychopathy.seas.upenn.edu [158.130.68.91]) by rhizome.seas.upenn.edu (8.13.6/8.12.8) with ESMTP id m64Ki96u022632 for <types-announce-nHFbR+4dATOoZA3Q9b/B0PZ8FUJU4vz8@public.gmane.org>; Fri, 4 Jul 2008 16:44:09 -0400
- Original-received: from lion.seas.upenn.edu (LION.seas.upenn.edu [158.130.12.194]) by psychopathy.seas.upenn.edu (8.13.6/8.12.10) with ESMTP id m64Ki8tj014808; Fri, 4 Jul 2008 16:44:08 -0400
- Original-received: from 192-168-0-7.rfc1918.fiberpipe.net (dsl-209-151-53-87.fiberpipe.net [209.151.53.87]) (authenticated bits=0) by lion.seas.upenn.edu (8.13.6/8.13.6) with ESMTP id m64Khx4R018783 (version=TLSv1/SSLv3 cipher=AES128-SHA bits=128 verify=NOT); Fri, 4 Jul 2008 16:44:08 -0400
- Original-sender: types-announce-bounces-nHFbR+4dATOoZA3Q9b/B0PZ8FUJU4vz8@public.gmane.org
- Original-x-from: types-announce-bounces-nHFbR+4dATOoZA3Q9b/B0PZ8FUJU4vz8@public.gmane.org Mon Jul 07 15:52:09 2008
- Xref: news.gmane.org gmane.comp.science.types.announce:800
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Types readers may find some harmless amusement in slides from a talk I gave at MFPS recently... http://www.cis.upenn.edu/~bcpierce/papers/harmful-mfps.pdf Enjoy, Benjamin
--- End Message ---
-- Jesse Alama (alama@stanford.edu)