From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id CC5AB8002D for ; Wed, 12 Oct 2016 09:11:51 +0200 (CEST) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=lego395@gmail.com; spf=Pass smtp.mailfrom=lego395@gmail.com; spf=None smtp.helo=postmaster@mail-pf0-f172.google.com Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of lego395@gmail.com) identity=pra; client-ip=209.85.192.172; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="lego395@gmail.com"; x-sender="lego395@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of lego395@gmail.com designates 209.85.192.172 as permitted sender) identity=mailfrom; client-ip=209.85.192.172; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="lego395@gmail.com"; x-sender="lego395@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-pf0-f172.google.com) identity=helo; client-ip=209.85.192.172; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="lego395@gmail.com"; x-sender="postmaster@mail-pf0-f172.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AfuWXIRBgAcKqW6yrAzn9UyQJP3N1i/DPJgcQr6Af?= =?us-ascii?q?oPdwSP79psbcNUDSrc9gkEXOFd2CrakV0ayK6uuxBSQp2tWoiDg6aptCVhsI24?= =?us-ascii?q?09vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6kO74TNaIBjjLw09?= =?us-ascii?q?fr2zQd+IyZjunLHus7ToICxwzAKnZr1zKBjk5S7wjeIxxbVYF6Aq1xHSqWFJce?= =?us-ascii?q?kFjUlhJFaUggqurpzopM0r221qtvkg789NV7nhN+R9FOQATWduD2dgz8TusVHn?= =?us-ascii?q?TBCTri8XW2AS1x5JGBTt7RfgX563vDGs5cRn3yzPHcTxXLkyVnyd5qFkAEvomT?= =?us-ascii?q?gOMTER6Gbdjdw2h6Ve9kHy7ydjypLZNdnGfMF1ebnQKJZDHTJM?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0AvCwCT4f1XhqzAVdFcGwEBAQMBAQEJA?= =?us-ascii?q?QEBFwEBBAEBCgEBgn0UAQEBAQF0fI07lnyHW48Lh30MPBABAQEBAQEBAQEBARI?= =?us-ascii?q?BAQEICwsJGS9BEIFhBAEVAQSCEAEBAQMBEigGATkDAQsBBQUYLiETAQUBHAYTI?= =?us-ascii?q?ogUAw8IAQ2oJYEyPjKQDAWEFycNg2wBCx0DAQUQiCoIglCCR4Uwgi8FjzWKGDW?= =?us-ascii?q?GJ4ZLgwuBWAEVh20xhWmIZYQBE4I9MYERNWEFB4EagUqCHlKDdoMtgUEBAQE?= X-IPAS-Result: =?us-ascii?q?A0AvCwCT4f1XhqzAVdFcGwEBAQMBAQEJAQEBFwEBBAEBCgE?= =?us-ascii?q?Bgn0UAQEBAQF0fI07lnyHW48Lh30MPBABAQEBAQEBAQEBARIBAQEICwsJGS9BE?= =?us-ascii?q?IFhBAEVAQSCEAEBAQMBEigGATkDAQsBBQUYLiETAQUBHAYTIogUAw8IAQ2oJYE?= =?us-ascii?q?yPjKQDAWEFycNg2wBCx0DAQUQiCoIglCCR4Uwgi8FjzWKGDWGJ4ZLgwuBWAEVh?= =?us-ascii?q?20xhWmIZYQBE4I9MYERNWEFB4EagUqCHlKDdoMtgUEBAQE?= X-IronPort-AV: E=Sophos;i="5.31,333,1473112800"; d="scan'208";a="196470007" Received: from mail-pf0-f172.google.com ([209.85.192.172]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 12 Oct 2016 09:11:50 +0200 Received: by mail-pf0-f172.google.com with SMTP id e6so14303933pfk.3 for ; Wed, 12 Oct 2016 00:11:50 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=sender:from:content-transfer-encoding:mime-version:subject:date :references:to:in-reply-to:message-id; bh=47XXhGVrxBgYkhhe2yiQz3cYqrPH0cW+Bcd/4JmlGEw=; b=dGjracwgXsrY8NDPQ82Vzs3NREa9Hbt09tVa+e9tHSIcWnYuyuLfcZS3jZuFrMHxeE VQnRUxMiL4ve3nBQs9M7H8eNcBPMKp3KG5EaX0HzwOLWR9o+QTDg4epRjF0NUyI7DH3P TK2ggXSCE5ODN/LfZShMBs0RffVGkAICvduW6O2GFZFjimKUQGK2zjoKDbmISV1nckih wnF6ETW6iU3V5w8jl6lQ5M3jQfrQnUURivSE1uayG+3ADK9cmi19imBvuoLq7QiLXkxu WhwnudmPqPx4c1FR4UH9CGxMdA53Bo23D7zrUjlf2BVSRPiLuj+omRBF1IJnobo/CaDL Eqwg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20130820; h=x-gm-message-state:sender:from:content-transfer-encoding :mime-version:subject:date:references:to:in-reply-to:message-id; bh=47XXhGVrxBgYkhhe2yiQz3cYqrPH0cW+Bcd/4JmlGEw=; b=UxTF21PfXioA6RA6PajaNd7ZkWbaFoosLw3XJE9tHILECMsgK9bEbqtx25zZms/z12 v8015xzPxtmBiPBFS9pntVvkJhPruxU7ch2TdRgwpK1xoeB93RM2VJeGFiDKB0WdXDKh hBRZXsxzzzowhFJUQZuCW0QImzFv7sznPTq1EgDNhrBKt35BXDiA4A23h1NszXAJpdX2 KrSx0bF2EpvyTm4i7teBijfhEN/FIE38YDt/VbEVoiLrY/JN2+YZhFk6UnSGaSog1mNc UhreB9VUEi3Eo48sj5Qg8Sm8ecCMNr+2KyN4SVcxRxtrroi3eqlmWS/+SZL42chjyiCK hzxg== X-Gm-Message-State: AA6/9RnnI4U7/dfHtoEINLiB8CFNrFQvp+TI3D4RaMk/t1Uea4pr1X6acjwN2mKftTgW0w== X-Received: by 10.98.4.6 with SMTP id 6mr2990709pfe.152.1476256308332; Wed, 12 Oct 2016 00:11:48 -0700 (PDT) Received: from ?IPv6:2602:306:c475:e300:4021:6fa:4db9:2bd1? ([2602:306:c475:e300:4021:6fa:4db9:2bd1]) by smtp.gmail.com with ESMTPSA id xs10sm9099948pac.24.2016.10.12.00.11.47 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 12 Oct 2016 00:11:47 -0700 (PDT) Sender: Haoyang Wang From: Haoyang Wang Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Mime-Version: 1.0 (Mac OS X Mail 10.0 \(3226\)) Date: Wed, 12 Oct 2016 00:11:44 -0700 References: <20161011235521.Horde.3X1jpLQmLKIbcZWI8PENsh5@webmail.in-berlin.de> To: Caml List In-Reply-To: Message-Id: <58C4E25E-1DEA-4276-85B5-2E45342E141D@pobox.com> X-Mailer: Apple Mail (2.3226) Subject: Re: [Caml-list] First-Class Types?! > On Oct 12, 2016, at 12:07 AM, Kakadu wrote: > Which languages already have first class types? Where can I read about it? Coq https://coq.inria.fr See also https://en.wikipedia.org/wiki/Lambda_cube Haoyang