Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-05-09

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary

All times shown according to UTC.

Time Nick Message
05:18 larsrh how about http://isabelle.in.tum.de/dist/Isabelle2016-1/doc/implementation.pdf?
05:54 pruvisto what about Larry Paulson's original paper from 1989-ish?
05:54 pruvisto I would expect that to have some descriptions of that
05:55 pruvisto albeit somewhat anachronistically
06:37 JCaesar OOh, someone did give a more comprehensive answer to my question about Isabelle soundness. https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2017-January/msg00000.html And I missed it. :(
06:39 pruvisto Ken Kubota's emails are in dire need of a TL;DR
06:53 ertes-w joined #isabelle
06:55 ertes-w left #isabelle
08:06 dave24 joined #isabelle
08:48 chindy pruvisto: you mean: "The Next 700 Theorem Provers" ? or which paper are you talking about specifically ?
09:00 pruvisto I think so
09:00 pruvisto but really that was just a hunch
09:01 pruvisto ALso, it's quite possible that not much of that original architecture remains today
09:02 pruvisto in particular, I think axiomatic type classes and overloading changed quite a few things
09:02 pruvisto You may have more luck asking on the mailing list
09:08 chindy thanks
09:10 pruvisto I'll get a big bucket of popcorn.
09:14 larsrh now that's just cruel
09:17 chindy :(
09:19 pruvisto chindy: I was serious; I do think that if you want to get a good answer, you'll have to ask there.
09:20 pruvisto But you might well start a medium-sized flame war with it.
09:28 larsrh maybe we need a documentation pdf called "How is theorem formed"
09:28 larsrh but in all seriousness, chindy, the pdf I linked above should contain the basic inference rules
09:29 larsrh in practise, things are more complicated because of multithreading
09:29 larsrh I don't think there's a good description of that around
09:30 larsrh there's http://www4.in.tum.de/~wenzelm/papers/parallel-isabelle.pdf from 2009 though
09:36 pruvisto larsrh: well what about overloading and axiomatic type classes?
09:47 tautologico joined #isabelle
09:51 larsrh pruvisto: classes are covered in implementation.pdf
09:51 larsrh not sure about general overloading
09:55 pruvisto larsrh: including the justification why they don't cause inconsistency?
09:57 kyagrd joined #isabelle
09:58 larsrh pruvisto: Is that what chindy asked for?
09:58 larsrh I thought they were looking for just a description
09:59 pruvisto True, I may have over-interpreted that request.
10:00 larsrh I can almost hear the crickets in the answer section of this question: https://stackoverflow.com/q/43849434/4776939
10:03 int-e well this question may be about 11 years late.
10:04 larsrh there was a thread on the mailing list last year about getting Isabelle2005 to run
10:04 larsrh but no mention of PG there
10:04 int-e otoh nobody seems to know why my auto command loops either :P
10:05 larsrh at least you're running a recent version of 'auto' :-)
22:54 ertes joined #isabelle
23:44 chindy pruvisto: yea i will probably ask on the weekend... gota talk with my professor first :), larsrh, i wasnt asking for this in particular, but I've been told that the type classes were believed to contain a bug shown by Kuncar(dont know how toe spell the name), however the concerns have been dealt with/argued for and should not pose further reason to assume an underlying inconsistency
23:45 chindy Also i am generally search for source on the theoretical background/underlying theory. Also anything on meta verification... basically anything intersting,  that i can read and includ in my thesis
23:46 chindy Thing is i found 2/3 great papers by T. Hales and Harrison, however both of them concern themselfs with HOL light, and since my project is using Isabelle, I was wondering if i could find anything similar for isabelle

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary