Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Differential Geometry Module Proposal

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Differential Geometry Module Proposal


Chronological Thread 
  • 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

 

cid:image001.png@01D41902.C62EECA0

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

PNG image




Archive powered by MHonArc 2.6.18.

Top of Page