From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <garrigue@math.nagoya-u.ac.jp>
X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr
X-Spam-Level: *
X-Spam-Status: No, score=1.1 required=5.0 tests=AWL,DNS_FROM_RFC_ABUSE,
	SPF_SOFTFAIL autolearn=disabled version=3.1.3
X-Original-To: caml-list@yquem.inria.fr
Delivered-To: caml-list@yquem.inria.fr
Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104])
	by yquem.inria.fr (Postfix) with ESMTP id 42C04BBC1
	for <caml-list@yquem.inria.fr>; Mon, 18 Feb 2008 11:05:40 +0100 (CET)
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: Ao8CAHfnuEeCNhAB/2dsb2JhbACrCA
X-IronPort-AV: E=Sophos;i="4.25,370,1199660400"; 
   d="scan'208";a="9298518"
Received: from kurims.kurims.kyoto-u.ac.jp ([130.54.16.1])
  by mail3-smtp-sop.national.inria.fr with ESMTP; 18 Feb 2008 11:05:38 +0100
Received: from localhost (orion [130.54.16.5])
	by kurims.kurims.kyoto-u.ac.jp (8.13.8/8.13.8) with ESMTP id m1IA5WsN002591;
	Mon, 18 Feb 2008 19:05:32 +0900 (JST)
Date: Mon, 18 Feb 2008 19:05:29 +0900 (JST)
Message-Id: <20080218.190529.45878855.garrigue@math.nagoya-u.ac.jp>
To: cconway@cs.nyu.edu
Cc: caml-list@yquem.inria.fr
Subject: Re: [Caml-list] Formal specifications of programming languages
From: Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>
In-Reply-To: <4a051d930802150630l20f46d17g153842c2cd70b1c2@mail.gmail.com>
References: <47B348F6.6010607@fmf.uni-lj.si>
	<47B40514.3070906@inria.fr>
	<4a051d930802150630l20f46d17g153842c2cd70b1c2@mail.gmail.com>
X-Mailer: Mew version 4.2 on Emacs 22.1 / Mule 5.0 (SAKAKI)
Mime-Version: 1.0
Content-Type: Text/Plain; charset=us-ascii
Content-Transfer-Encoding: 7bit
X-Spam: no; 0.00; ocaml:01 didier:01 formalized:01 didier:01 polymorphic:01 polymorphic:01 abstract:01 encode:01 caml-list:01 remy:01 remy:01 modules:02 encoding:02 objects:02 garrigue:03 

From: "Christopher L Conway" <cconway@cs.nyu.edu>

> Do any of these papers address existentials?

There are no existentials in ocaml, only first-class universal types
(in polymorphic methods and polymorphic record fields.)
Universal types can be used to encode existentials through the usual
dual encoding.
The theory behind polymorpic methods is described in my paper with
Didier Remy, in the Objects section. Polymorphic fields in records are
simpler, and they were already formalized in earlier papers by Didier
Remy.

(Actually, abstract types in modules can also be seen as existentials,
but I don't think this is what you are talking about.)

Jacques Garrigue