Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-05-03

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

All times shown according to UTC.

Time Nick Message
01:48 ilbot3 joined #isabelle
01:48 Topic for #isabelle is now Official channel for the Isabelle/HOL theorem prover: http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html || Now with logging: http://irclog.perlgeek.de/isabelle/
07:41 ertes joined #isabelle
07:58 dave24 joined #isabelle
15:06 chindy are there any papers on the correctness/soundness of isabelle/core ... =
15:06 chindy ?
15:10 larsrh https://www21.in.tum.de/~kuncar/
15:10 larsrh last four papers are related to that
15:41 pruvisto "There are no bugs in the Isabelle kernel." Makarius Wenzel, Private Communication
15:41 pruvisto actually, Public Communication
15:42 pruvisto also, Isabelle does not have a kernel. Also Makarius Wenzel. :P
16:10 chindy does not have a Kernel ?
16:10 chindy isnt isabelle LCF style
16:12 int-e well, there are no bugs, there is no kernel, so how could there be bugs in the kernel?
16:14 int-e To my limited understanding, the "kernel" isn't exactly small (it does higher order unification, for example), and it's not quite possible to separate the ML files into a kernel and the rest.
16:19 pruvisto int-e: there is some ongoing work about moving unification out of the kernel completely
16:19 pruvisto there are still some technical and political issues, but we're on it
16:19 pruvisto and by "we", I mean "not me", but people here in Munich
16:20 pruvisto chindy: it is (sort of), but there are arguably some violations of that
16:20 pruvisto you can have oracles, and the information about what has gone through the kernel and what was proven with oracles is not tracked very reliably
16:21 pruvisto also, you can have "proof futures" for parallelisation and they can cause issues
16:21 pruvisto I don't understand half of the issue, but… it's complicated.
16:22 chindy can i ask, who is on it, I image they have some paper etc. on it
16:41 ertes joined #isabelle
17:16 pruvisto chindy: Simon Wimmer and Fabio Madge Pimentel
17:17 pruvisto There is this: http://www.in.tum.de/~nipkow/Isabelle2016/Isabelle2016_11.pdf
17:17 pruvisto oh, or did you not mean the unification stuff?
17:17 pruvisto what did you mean?
17:18 pruvisto If you did mean Unification, Fabio Madge Pimentel did his BSc thesis on it, but I cannot seem to find it online
19:23 ertes joined #isabelle
22:04 ertes joined #isabelle

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