coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Differential Geometry Module Proposal

From: Thomas Burdick <tfb AT cadence.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Differential Geometry Module Proposal
Date: Mon, 13 Aug 2018 06:40:59 +0000
Accept-language: fr-FR, en-US
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=tfb AT cadence.com; spf=Pass smtp.mailfrom=tfb AT cadence.com; spf=Pass smtp.helo=postmaster AT NAM02-BL2-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:7K2AEh81zdyFLP9uRHKM819IXTAuvvDOBiVQ1KB31e4cTK2v8tzYMVDF4r011RmVBduds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+55zebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRh/2hikaKz43/mLZisJyg61VoRKuuxNwzpXOYI2JMfpzZL/RcMkYSGdHQ81fVzZBAoS5b4YXEeQBPeFYr4znqFsVsBCzGBSsBPnyxT9JmnD23rAx3uM9EQHIxwMtBM4Bv27Jo9rrMqcdTf66wLPUwjXEavNbwDHw45XGfBAmpPGDR7NwcczJxEYzDQzKk0ufqYr5MDyLzOgCr2+b7+9mWOmyiGAnsxl8riWzysojkIXEiYAYxkrK+Ch62oo4JN21RFZmbdOnEJZcrT+WO5Z0T884XW1luCg3xqcGtJO/ZCQKxoooyh3DZ/GCdoWH+A7sW/yeLDp9hX9oebayiAy3/Ee6yuDxVsa53VNOoydFj9XMuHYA3AHJ5MedUPty5EKh1C6P1w/N7uFEJlg5m7LHJpAm3rI8iIMfvFnFECPogUn2i7SZeVs+9uiv9uTnfq7pppiBN49ylw7yKLwumta4AeQkLAcBQ3Sb+eW71L3l50H5R6hKjuEykqnet5DaJt4XqbK+Aw9Qyooj6hC/ACm60NkAgHULMF1IdAiIgoXrIV3DLvP1Ae2+jlmsiDtrwurJPrzlApXDNHjDl7LhcK5h605S0wU+1sxQ6IhJBb4fJvL8RlH+uMbEAR8+Ngy42/znB8ll1oMCRWKPBbeUP7/VsV+R/+4gP+2MZJIOtzvmMPgk5/vujWcjllMHfKmp24EXaHGiEfh8LUWZeymkvtBUW2wNp081SPHgoFyESz9aIXioFepo7TYiTYmiEI3rR4a3gbXH0j3tTbNMYWUTNlCLFH7zP6+ZQfsNYyHadtNvmBQPXLSsTYQskxqpsVmpmPJcMuPI93hA5trY399v6riLzEBgxXlPF82Yllq1YSRxl2IMSSUx2fkk80d0xlqF2qU+iPtdR4UKu6F5FzwiPJuZ9NRUTsjoU1uaLNyARFugSdjgCjY0HIpono0+Jn1lEtDntSjtmiqnB7hJyO6tLblsqOf2+yK0IMxwjXHbyKMmkl8qBNNVMnGrjbJ+8A6VAJPVl0KelOChcqFOhSM=
Spamdiagnosticmetadata: NSPM
Spamdiagnosticoutput: 1:99

I'm not aware of any such modules in Coq, but I'd be very interested to hear of any progress you make here!

Bon courage!

Thomas

Thomas BURDICK | Principal Services AE

P: +33 1 34 88 53 66 www.cadence.com

De : <coq-club-request AT inria.fr> au nom de Larry Lee <llee454 AT gmail.com>
Répondre à : "coq-club AT inria.fr" <coq-club AT inria.fr>
Date : jeudi 9 août 2018 à 20:31
À : "coq-club AT inria.fr" <coq-club AT inria.fr>
Objet : [Coq-Club] Differential Geometry Module Proposal

EXTERNAL MAIL

Hi,

I'm looking for mathematical fields that currently do not have any contributed developments and noticed that none of the modules listed in the Coq Package Index appeared to cover differential geometry. I'd like to develop a module covering basic results, but I'd like to avoid duplicating existing work. Does anyone know of any Coq modules that cover Differential Geometry? If not, would anyone like to share any recommendations/requests concerning the new module?

Thanks,

- Larry Lee

[Coq-Club] Differential Geometry Module Proposal, Larry Lee, 08/09/2018
- Re: [Coq-Club] Differential Geometry Module Proposal, Li-yao Xia, 08/09/2018
- Re: [Coq-Club] Differential Geometry Module Proposal, Thomas Burdick, 08/13/2018