From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from lists.gentoo.org ([140.105.134.102] helo=robin.gentoo.org) by nuthatch.gentoo.org with esmtp (Exim 4.60) (envelope-from ) id 1Futky-0000QX-RB for garchives@archives.gentoo.org; Mon, 26 Jun 2006 16:16:13 +0000 Received: from robin.gentoo.org (localhost [127.0.0.1]) by robin.gentoo.org (8.13.7/8.13.6) with SMTP id k5QGEhXr016942; Mon, 26 Jun 2006 16:14:43 GMT Received: from web31715.mail.mud.yahoo.com (web31715.mail.mud.yahoo.com [68.142.201.195]) by robin.gentoo.org (8.13.7/8.13.6) with SMTP id k5QGEfpx022966 for ; Mon, 26 Jun 2006 16:14:42 GMT Received: (qmail 38078 invoked by uid 60001); 26 Jun 2006 16:14:40 -0000 DomainKey-Signature: a=rsa-sha1; q=dns; c=nofws; s=s1024; d=yahoo.com; h=Message-ID:Received:Date:From:Subject:To:In-Reply-To:MIME-Version:Content-Type:Content-Transfer-Encoding; b=ywY2eCX5A+y7hHq5r6aOs15gZipEVmZXfVPCQbRPIppBllqz92JLhXDyafvmWSXU40BcRLwILo3TE5XxsXRE6fwkjkEQuB1r/lFAM06pIl/auSfPO0/XR4l+0JZubPdR8z5v//70Xu78MWT1mv9fsMCEt0F8FcpwL2kR080fkPc= ; Message-ID: <20060626161440.38076.qmail@web31715.mail.mud.yahoo.com> Received: from [216.174.43.195] by web31715.mail.mud.yahoo.com via HTTP; Mon, 26 Jun 2006 09:14:40 PDT Date: Mon, 26 Jun 2006 09:14:40 -0700 (PDT) From: C Y Subject: [gentoo-science] sci-proof To: gentoo-science@lists.gentoo.org In-Reply-To: <20060626150909.GA22327@ubik> Precedence: bulk List-Post: List-Help: List-Unsubscribe: List-Subscribe: List-Id: Gentoo Linux mail X-BeenThere: gentoo-science@gentoo.org Reply-to: gentoo-science@lists.gentoo.org MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Transfer-Encoding: 8bit X-Archives-Salt: ab00dc4b-a58b-42cb-a616-167391fe755e X-Archives-Hash: bc0f9aa0bea776eac39eb13947919e89 --- Alexandre Buisse wrote: > Sign me up for sci-proof (even if it is only a subset of > sci-mathematics). As far as I know, there is only coq, but I am > working on adding agda, and we'll see from there... I know of coq and otter in the "already present" category. Candidates for inclusion: Isabelle (the devs don't see the need for a package - fair warning) HOL http://hol.sourceforge.net/ Mizar (anybody know what the license is?) http://www.mizar.org IMPS http://imps.mcmaster.ca/ (I think the license looks OK, but it would probably need to be added to portage.) nqthm http://www.computationallogic.com/software/nqthm/, maybe http://www.computationallogic.com/software/pc-nqthm/ as well (might be a bit dated now, but probably still worth including - it's GPL) ProofPower http://www.lemma-one.com/ProofPower/index/ PVS has a problematic license - it could be set up but I'm not sure if it's worthwhile. NuPrl http://www.cs.cornell.edu/Info/Projects/NuPrl/ - this is another one where I can't find the license, but it's an excellent candidate for inclusion. Larch might be of interest - http://www.sds.lcs.mit.edu/spd/larch/ MetaPRL http://metaprl.org/ Also interesting might be the Pcoq interface, although I don't know if it is maintained any longer: http://www-sop.inria.fr/lemme/pcoq/ I'm sure I missed a few. Anyway, certainly enough to start :-). Cheers, CY __________________________________________________ Do You Yahoo!? Tired of spam? Yahoo! Mail has the best spam protection around http://mail.yahoo.com -- gentoo-science@gentoo.org mailing list