The Coq mailing list

[Christopher Dutchyn <dutchyn AT cs.usask.ca>]

I show undergrads a proof that a simple balanced binary tree implementation 
is balanced.  It fits with the course material at that time, where they are 
learning about balanced trees.

ChrisD

> On Jan 30, 2015, at 14:01, Eric Mullen 
> <emullen AT cs.washington.edu>
>  wrote:
> 
> If you wanted to give a 10 minute demo to show off how cool Coq was, what 
> example would you use?
> 
> Specifically, if you were talking to a bunch of undergraduates in Computer 
> Science, and you had 10 minutes to convince them that Coq was an awesome 
> research tool, what would be your go to example?
> 
> Ideas so far have been:
>  * Implementing slow and fast Fibonacci functions, and proving they 
> calculate the same thing
>  * Proving that the identity function and the Fibonacci function are both 
> monotonic
> 
> I'm leaning towards the second due to its simplicity, but I would very much 
> appreciate small examples which illustrate how cool it is to write code and 
> prove properties about it.
> 
> Thanks much,
> Eric Mullen