Stream: Coq users

Topic: ✔ What happened to CAD?


view this post on Zulip Luigi Massacci (Feb 01 2024 at 17:03):

Yes, whose history if I’m not mistaken starts with this paper and then continues on over a couple others

view this post on Zulip Cyril Cohen (Feb 01 2024 at 17:12):

The CAD has been implemented in Coq indeed by Assia Mahboubi. However the formal proof was never completed. Mathcomp did not exist at the time. Many years later with Boris Djalal, we tried to reprogram and prove it using https://github.com/math-comp/real-closed and https://github.com/math-comp/cad. But this was never finished.

view this post on Zulip Luigi Massacci (Feb 01 2024 at 17:26):

Got it, thank you

view this post on Zulip Notification Bot (Feb 01 2024 at 17:26):

Luigi Massacci has marked this topic as resolved.


Last updated: Jun 23 2024 at 04:03 UTC