Timeline for Between mu- and primitive recursion
Current License: CC BY-SA 2.5
5 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Dec 29, 2010 at 10:12 | vote | accept | CommunityBot | moved from User.Id=10891 by developer User.Id=35352 | |
| Dec 14, 2010 at 15:49 | comment | added | kow | References is perhaps overstating it. I've learnt about it in the context of proof assistants for higher-order logic (e.g. Isabelle/HOL) and type theory (e.g. Coq). All these have extensive online documentation and examples (and have been used for major proofs, e.g. Gonthier's proof of the four color theorem). You might also look at the chapter on finite type arithmetic in Troelstra&van Dalen's Constructivism in Mathematics, Vol 2, for more background. It might also interest you to think about what can be done with an NNO in a Cartesian Closed Category -- exponentials are very useful. | |
| Dec 10, 2010 at 18:07 | comment | added | user10891 | This is very helpful answer and I might have rushed when flagging answer (I wasn't expecting more answers). Thank you for writing this up anyway! Kow, do you happen to have any references in hand for any applications of this method? | |
| Nov 29, 2010 at 21:08 | comment | added | Max | Thank you for adding this! I was sorry to see an answer accepted without this approach being mentioned, when it seems to me to be more useful for real programming. I wanted to mention it myself, but it was not something I was in a position to look up or work out myself when I made my original answer: I was invigilating an exam. | |
| Nov 23, 2010 at 13:54 | history | answered | kow | CC BY-SA 2.5 |