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):
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png)
timeasmymeasure
no subject
Date: 2007-06-02 02:03 am (UTC)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..
Кроме того, там были разные интересные люди..
А вчера -- у некоторых был джаз, а у некоторых -- электронная музыка :-)))