coq-club AT inria.fr
Subject: The Coq mailing list
List archive
Re: [Coq-Club] Fwd: Fellowship Opportunity for < 5 yrs from PhD - Power of Information
Chronological Thread
- From: 1337 777 <1337777.ooo AT gmail.com>
- To: Vladimir Voevodsky <vladimir AT ias.edu>, coq-club AT inria.fr, fellowship AT templetonworldcharity.org
- Cc: Yves.Bertot AT inria.fr
- Subject: Re: [Coq-Club] Fwd: Fellowship Opportunity for < 5 yrs from PhD - Power of Information
- Date: Wed, 30 Nov 2016 08:37:04 -0800
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=1337777.ooo AT gmail.com; spf=Pass smtp.mailfrom=1337777.ooo AT gmail.com; spf=None smtp.helo=postmaster AT mail-oi0-f65.google.com
- Ironport-phdr: 9a23:n++hix31rsKY9NzHsmDT+DRfVm0co7zxezQtwd8ZsegQLfad9pjvdHbS+e9qxAeQG96KsLQf2qGJ4uigATVGusnR9ihaMdRlbFwst4Y/p0QYGsmLCEn2frbBThcRO4B8bmJj5GyxKkNPGczzNBX4q3y26iMOSF2kbVImbsy8IIPZjty22uau4NWTJlwQ3HvuKY91eSuypAnQs8gMybVlJ7g2xgDKszMcZeBfyWJtJEi7nh/noMq84cgnuy9Xorcq89NKeaT8ZaUxC7JCSHwoPmQx49LwtRjbZReC42MYX3kRlAVPGQzJ5xHzRJbto239rOUu9jOdOJivFutrEWv9sO8/EUSz13hYaHg+92b/hcl5jaYdqxWk8U8si7XIaZ2YYaItNpjWeskXEC8YBp5c
Proph Voevodsky
https://1337777.github.io/init.html
solves some question of Bertot [fn:1] which is how to communicate COQ math programming. Some finding is that the information-technology enabled by the _EMACS org-mode_ [fn:2] logiciel is effective to communicate _timed-synchronized_ _geolocated_ _simultaneously-edited_ _multi-authors_ _searchable_ text, and therefore to communicate textual COQ math programming.
For instance, the wiki-style https://github.com/1337777/1337777.github.io is the output of some automated _continuous-integration_ (periodic-pull, make emacs org, make coq, push) bash script [fn:3] which shall periodically input changes from everybody ( merge-conflict seniority-sorted ... ) github-repositories if it is by-chance named « OOO1337777 » . Some corresponding logiciel [fn:4] [fn:5] shall enable webcitations / reviews.
Memo that the common writing of mathematics using /vertically stacked/ symbols or /large/ symbols is mostly not necessary both from the prettiness angle of view ( /.PDF obsession/ ) or from the sensible-encoding angle of view. In this sense, the combination of all the techniques of the COQ computer and the SSREFLECT style is sufficient to do mathematics at least at the most-meta encoding ( /temporal-deductions by the bio-memory/ ).
This angle of view also solves some question of templetonworldcharity.org [fn:6] which is how information(-technology) enables the communication of discoveries with the motivation of affecting permanent impact : onto both the scholarly class and the wider public , by both the predictable logical method and the dia-para-logical randomness of reality .
[fn:1] ~Bertot~
[[https://team.inria.fr/marelle/advanced-coq-winter-school-2016-2017/]]
[fn:2] [[http://alan.petitepomme.net/tips/executing_coq.html]]
[fn:3] ~1337777.OOO~ [[https://github.com/1337777/OOO1337777/blob/master/makegit.sh.org]]
[fn:4] ~1337777.OOO~ [[http://1337777.link/ooo/guJAH-jSeQcTEST/2016/1/5/11/9/11/1]]
[fn:5] ~1337777.OOO~ [[https://github.com/1337777/upo/blob/master/editableTree.urp]]
[fn:6] [[http://www.templetonworldcharity.org/what-we-fund/core-funding-areas/big-questions]]
https://1337777.github.io/init.html
solves some question of Bertot [fn:1] which is how to communicate COQ math programming. Some finding is that the information-technology enabled by the _EMACS org-mode_ [fn:2] logiciel is effective to communicate _timed-synchronized_ _geolocated_ _simultaneously-edited_ _multi-authors_ _searchable_ text, and therefore to communicate textual COQ math programming.
For instance, the wiki-style https://github.com/1337777/1337777.github.io is the output of some automated _continuous-integration_ (periodic-pull, make emacs org, make coq, push) bash script [fn:3] which shall periodically input changes from everybody ( merge-conflict seniority-sorted ... ) github-repositories if it is by-chance named « OOO1337777 » . Some corresponding logiciel [fn:4] [fn:5] shall enable webcitations / reviews.
Memo that the common writing of mathematics using /vertically stacked/ symbols or /large/ symbols is mostly not necessary both from the prettiness angle of view ( /.PDF obsession/ ) or from the sensible-encoding angle of view. In this sense, the combination of all the techniques of the COQ computer and the SSREFLECT style is sufficient to do mathematics at least at the most-meta encoding ( /temporal-deductions by the bio-memory/ ).
This angle of view also solves some question of templetonworldcharity.org [fn:6] which is how information(-technology) enables the communication of discoveries with the motivation of affecting permanent impact : onto both the scholarly class and the wider public , by both the predictable logical method and the dia-para-logical randomness of reality .
[fn:1] ~Bertot~
[[https://team.inria.fr/marelle/advanced-coq-winter-school-2016-2017/]]
[fn:2] [[http://alan.petitepomme.net/tips/executing_coq.html]]
[fn:3] ~1337777.OOO~ [[https://github.com/1337777/OOO1337777/blob/master/makegit.sh.org]]
[fn:4] ~1337777.OOO~ [[http://1337777.link/ooo/guJAH-jSeQcTEST/2016/1/5/11/9/11/1]]
[fn:5] ~1337777.OOO~ [[https://github.com/1337777/upo/blob/master/editableTree.urp]]
[fn:6] [[http://www.templetonworldcharity.org/what-we-fund/core-funding-areas/big-questions]]
- Re: [Coq-Club] Fwd: Fellowship Opportunity for < 5 yrs from PhD - Power of Information, 1337 777, 11/30/2016
Archive powered by MHonArc 2.6.18.