Functional programming at Harvard

[anhinga_anhinga]

Informal meeting, Friday, June 1:

https://lists.ccs.neu.edu/pipermail/pl-seminar/2007/000390.html

Comments

[http://users.livejournal.com/_rowan_tree_/]

Пойдешь? Расскажешь?

[anhinga-anhinga.livejournal.com]

Во всяком случае, я написал им, что пойду (которые напишут до вторника, тем дадут бесплатное грызло на ланч ;-))..

Попробую рассказать, насколько смогу..

[anhinga-anhinga.livejournal.com]

Это было замечательно..

The best was the talk by Stephanie Weirich who stated a goal of replacing the "write-only" tech reports with computer-checked math! She even threatened to give a workshop "How to write your next POPL paper in Coq" at the next POPL :-)

Remarkably enough their code for the proof assistant looks like a reasonable functional programming code (some other speakers demonstrated rather horrible code for the same proof assistant):

http://www.chargueraud.org/arthur/research/2007/binders/

This group tries pretty hard to develop nice readable formal proofs and to teach others how to do this..

Кроме того, там были разные интересные люди..

А вчера -- у некоторых был джаз, а у некоторых -- электронная музыка :-)))

[http://users.livejournal.com/_rowan_tree_/]

Ага, пасиб.
Proofs for recursively defined structures should look like functional code - it's the nature of the beast! ;-)