coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Series / Real Analysis in Coq?

From: Bas Spitters <b.a.w.spitters AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Series / Real Analysis in Coq?
Date: Fri, 12 Jan 2018 13:09:18 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=b.a.w.spitters AT gmail.com; spf=Pass smtp.mailfrom=b.a.w.spitters AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f182.google.com
Ironport-phdr: 9a23:I4lsIBY2864rpNRya13X4JD/LSx+4OfEezUN459isYplN5qZr86/bnLW6fgltlLVR4KTs6sC17KP9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCagbb9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjm58axlVAHnhzsGNz4h8WHYlMpwjL5AoBm8oxBz2pPYbJ2JOPZ7eK7WYNEUSndbXstJVSNBDIOyYYUMAeQcI+hXs5Lwp0cSoRakGQWgGP/jxz1Oi3Tr3aM6yeMhEQTe0QE9Bd0Oq2nfosjtNKcTTeC10LfHzS/Yb/hL3jry85LEfQo7rfCCR75watLRyUgzFwPZkFqQs5flMiia1uQIqWeb7u5gWfizhG4grgF8uz6izdoihInOg4Ia0FHE9SNhzYY0I924Uk97bsS+HJterSGWL4R2QsI+Q2FopSY10acKtoK8fCgPzpks2h3Ra+SffoSW/h7uUPydLDR4iX5/Zr6zmQq+/VK9xuD/SMW51ktBoDBfndnWrH8N0gTe6siZRft5+UeswTOP2BrS6uFAOEw0jKnbJ4I4zr4+i5YeslrPEjX5mEXxi6+WeUEk9fay5+v7ZbXmo4eQN45yig7gLqQjgtKzDfg8PwQUXGWW+f6w2KP98UHlWrlGk/47nrfBvJDfP8sbp6q5AwFP0oYk7hayFyyp3M4CknUdIlNJYgmHj5DoO1HSPPD3E+2/g0+3nTdkwvDJJLzhApHXInffl7fheK5x61RAxwor0dBf+5VUB6kdL/L0Q0/9rcDXDhskMwOv2OvnE9V81oYGWW2VGKOZMaXSsUWJ5u01OeWMapUV637BLK0O4OempnskkxdJdq6wmJATdXqQH/J8Ikzfb2C60fkbFmJflAMlBNfyiUGeXCRILyK4Gat6+XcgEIO6EYrZXaiihbWA2GGwGZgANTMOMUyFDXq9L9bMYPwLci/HZ5Y5ymVVB4jkcJco0FSVjCG/zrNmKuTO/ShB7MDs0dF046vYkhRgrGUoXfTY6HmESiRPpk1NXyU/hfktrkl0y1PF2q990aQBSI5joshRWwJ/Dqbyiux3D9eoBFDEd9aNDU+lGpCoWGFrCN02xNAKbgB2HNDw1h0=

coquelicot.saclay.inria.fr/
Or if you want to be constructive:
https://github.com/c-corn

Bas

On Fri, Jan 12, 2018 at 12:36 PM, Siddharth Bhat
<siddu.druid AT gmail.com>
wrote:
> Hello all,
>
> I'm taking a signals and systems course this semester, so I was interesting
> in formalizing results on LTI systems in Coq. I've mostly dabbled with it in
> terms of software foundations, never on the math side.
>
> So, is there a formalization of real analysis ideas, such as sequences,
> series, etc? What about linear algebra?
>
> I tried searching "mathematical components", but it's a little too large to
> check out :)
>
> Cheers,
> Siddharth
>
>
> --
> Sending this from my phone, please excuse any typos!

[Coq-Club] Series / Real Analysis in Coq?, Siddharth Bhat, 01/12/2018
- Re: [Coq-Club] Series / Real Analysis in Coq?, Bas Spitters, 01/12/2018