The Coq mailing list

[1337 777 <1337777.net AT gmail.com>]

Professor Chlipala, You may report the COQ ICFP 2015 VANCOUVER SEMINAR using this site, as for the COQ ITP 2015 NANJING SEMINAR :

http://1337777.info/o1/049d5492bf0a3942b8a051a11abf3a11c8ffaf21a94c95c80ee28a0cb4b59b97b5c15d1fbb2dc9ff17242f7bbd82f26be2804acb33932b6220a8786330730cae6f

https://github.com/1337777/upo/blob/master/editableTree.urp

Initial attempt to motivate 2 questions :

1. Simultaneously doing tradeability profit and very technical computers/mathematics (contrast to php n00bs) is possible

2. for practical legal: separate ( « possibly-questionable » ) content from references, fuzzy or random ( none « intent/motive/know » ) references, alternative non-textual iconography interface;

for authoring: inbrowser confirmation of (ecdsa) public id same as author of message;

for tutor: timed browsing, geolocated references;

for simultaneous edit: « sub- » style for references, « mod- » style for xslt edit of content 

On Sun, Aug 9, 2015 at 11:08 PM, Adam Chlipala <adamc AT csail.mit.edu> wrote:

Are you planning to attend the ICFP 2015 conference <http://icfpconference.org/icfp2015/>?  If so, and presuming that subscription to coq-club implies an interest in the evolution of Coq as both a research project and a piece of infrastructure, then please drop me a line.  We are organizing an informal discussion at the conference about those topics, with some Inria representatives, and I'd like to know who might like to join in. Participation from both academia and industry is very welcome. Thanks!