Timeline for Wanted: a "Coq for the working mathematician"
Current License: CC BY-SA 3.0
30 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 28, 2021 at 10:12 | answer | added | Dima Pasechnik | timeline score: 7 | |
| Dec 9, 2017 at 13:55 | comment | added | Dima Pasechnik | by the way, there are 3 volumes there now (since Sept 2017?): softwarefoundations.cis.upenn.edu | |
| Jul 25, 2017 at 8:47 | answer | added | user48801 | timeline score: 16 | |
| Oct 26, 2016 at 2:39 | comment | added | Todd Trimble | Have a Coq and a smile... | |
| Oct 26, 2016 at 1:46 | history | edited | darij grinberg | CC BY-SA 3.0 | added 680 characters in body |
| Jul 2, 2016 at 17:38 | answer | added | James Smith | timeline score: 7 | |
| Jul 9, 2015 at 9:39 | comment | added | Włodzimierz Holsztyński | @MarkDickinson -- thank you. Thus does "sudo port" is a special port in Mac? I'll have to read this whole thread anew. | |
| Jul 8, 2015 at 18:24 | comment | added | Mark Dickinson | @WłodzimierzHolsztyński: If you have MacPorts, a sudo port install coq is all you need. If you're an Emacs user, you might also want to do sudo port install ProofGeneral, though the version there is a bit old, and I ended up downloading and installing the most recent ProofGeneral source. | |
| Jan 5, 2015 at 9:34 | comment | added | Włodzimierz Holsztyński | How do you start? Do you install Coq on your computer? How? (On MacBook Pro?). What computer environment do you need? | |
| Jan 4, 2015 at 23:49 | history | edited | darij grinberg | CC BY-SA 3.0 | added 457 characters in body |
| Jan 28, 2014 at 17:25 | comment | added | Andrej Bauer | You should start with plain Coq. | |
| Jan 28, 2014 at 16:16 | comment | added | Qfwfq | "I'm abstractly interested in [...]". LoL, only a mathematician could have used that adverb in a positive sense :) | |
| Jan 28, 2014 at 16:02 | history | edited | darij grinberg | CC BY-SA 3.0 | added 285 characters in body |
| Jan 28, 2014 at 16:01 | comment | added | darij grinberg | Thanks, but will this allow me to use CoqIDE in Windows? I've been trying to install it on a virtualized Ubuntu so far, but the dependencies don't play well... | |
| Jan 28, 2014 at 15:20 | comment | added | Neil Strickland | @darijgrinberg: About a year ago I tried to install ssreflect and could not get anywhere, but today I saw this page, which seems promising: mhtsai208.blogspot.co.uk/2010/10/… I haven't tried it yet, though. | |
| Jan 28, 2014 at 15:15 | comment | added | darij grinberg | Ouch. Am I seeing it right that ssreflect can only be used if Coq has been compiled from source? | |
| Jan 28, 2014 at 15:05 | comment | added | darij grinberg | Nice, thank you -- I haven't seen any kind of ssreflect tutorials so far. | |
| Jan 28, 2014 at 14:28 | comment | added | Lierre | That is not a book but still a good and recent introduction to Coq and SSReflect : www-sop.inria.fr/manifestations/MapSpringSchool It is the website of a spring school on Coq, it contains slides, exercises and solutions. | |
| Jan 28, 2014 at 13:10 | comment | added | darij grinberg | @AndrejBauer: This is interesting! Youtube wasn't on my list of places I was searching for tutorials. (That said, a PDF transcript would still be very nice -- it is much easier to switch between CoqIDE and a PDF window than to switch between CoqIDE and Youtube and play/pause the video all the time). | |
| Jan 28, 2014 at 13:08 | comment | added | darij grinberg | @SteveHuntsman: This is something I thought first, but it seems to me now that HoTT really has a rather orthogonal objective to what I want (vanilla constructivism, in as far as such a thing exists, and practice rather than theory, in as far as mathematics can be practical). | |
| Jan 28, 2014 at 13:04 | comment | added | Andrej Bauer | In France the non-mathematician would assume that after a hard day's work the mathematician wishes for a tasty coq au vin. | |
| Jan 28, 2014 at 10:52 | comment | added | shane.orourke | @WlodzimierzHolsztynski I would assume it's pronounced just like `cock'. | |
| Jan 28, 2014 at 10:26 | comment | added | Włodzimierz Holsztyński | How do you pronounce "Coq"? | |
| Jan 28, 2014 at 10:22 | comment | added | shane.orourke | I wonder what a non-mathematician would make of the title of this question... | |
| Jan 28, 2014 at 10:07 | answer | added | Neil Strickland | timeline score: 26 | |
| Jan 28, 2014 at 6:15 | comment | added | Andrej Bauer | Apologies for self-advertisment. To get you off the ground there are my Coq video tutorials at math.andrej.com/2011/02/22/… In general, I am afraid, it will be hard to get what you're looking for. As a pedagogical project I set up a formalization of reals at github.com/andrejbauer/dedekind-reals, that will show you how to "unorganize" yourself. Those files purposely do not contain anything fancy, and if you play through some of the less scary proofs you might learn a few tricks. | |
| Jan 28, 2014 at 5:42 | comment | added | David Roberts♦ | I presume you aware of the coq-club list? And there is groups.google.com/forum/#!forum/hott-amateurs as well as groups.google.com/forum/#!forum/homotopytypetheory | |
| Jan 28, 2014 at 4:22 | comment | added | Steve Huntsman | My spidey sense tells me that you'll find it either a) in the references (formal and informal) to the HoTT book or b) not at all | |
| Jan 28, 2014 at 4:12 | history | edited | Ricardo Andrade | the tag 'pony-request' had to go... | |
| Jan 28, 2014 at 4:01 | history | asked | darij grinberg | CC BY-SA 3.0 |