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):
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png)
timeasmymeasure
no subject
Date: 2007-05-25 06:08 pm (UTC)no subject
Date: 2007-05-25 06:24 pm (UTC)no subject
Date: 2007-05-25 06:35 pm (UTC)Попробую рассказать, насколько смогу..
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..
Кроме того, там были разные интересные люди..
А вчера -- у некоторых был джаз, а у некоторых -- электронная музыка :-)))
no subject
Date: 2007-06-02 02:32 am (UTC)Proofs for recursively defined structures should look like functional code - it's the nature of the beast! ;-)