The Coq mailing list

[FOURNIER Laurent <laurent.fournier AT irt-saintexupery.com>]

Hi all !

 

First, thank you all for your answers on this post, and for these good ideas to go further. I will probably come back with other questions.

 

There was a mistake in the sent code, so I fix it and rewrote it here:

https://github.com/pelinquin/eurofranc/blob/master/opti.py

 

By the way, I’m working at IRTSE (Toulouse) in a just started project dedicated to “system engineering” meaning a way to interface and integrate multi-domains models.

 

Having a request to the CoQ community seems to be a great case-study because it’s usually too hard for a system engineer to learn how to use this tool, while CS researchers can provide a great adding value and expertise by “building the formal proof” of properties on a given algorithm. I have to think how to make this process easier and the example on ‘Merchant Sharing Theory’ may be a good practice.

 

If things go well, I may look for a CoQ expert to co-write a paper on this experimentation.

Please contact me if you are interested.

 

Laurent