Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2016-01-14

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

All times shown according to UTC.

Time Nick Message
02:48 ilbot3 joined #isabelle
02: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/
02:55 spacekitteh-work where can i find documentation about the kernel?
05:21 spacekitteh joined #isabelle
08:50 ThreeOfEight spacekitteh: probably mostly the implementation manual: https://isabelle.in.tum.de/dist/Isabelle2015/doc/implementation.pdf
08:51 ThreeOfEight but I think Makarius's doctrine is "the code is the documentation"
08:53 ThreeOfEight but the implementation describes it in some detail
08:53 ThreeOfEight There are also some older papers by Larry Paulson that describe what the Isabelle kernel looked like in the early 90s
08:53 ThreeOfEight I think some aspects of it didn't change that much since then, but I might be mistaken
08:56 larsrh many parts of thm.ML are still the real thing
08:57 larsrh e.g. bicompose_aux
08:58 larsrh (** Add new theorem with prop = '[| Bs; As |] ==> C' to thq **)  <-- this comment is from 1993
08:58 larsrh (well, or possibly older)
08:59 larsrh the first revision in the repository is from 1993-09-16
09:00 spacekitteh thanks
09:00 spacekitteh i wanna try making the core lambda calculus more expressive
09:20 JCaesar joined #isabelle
16:19 zachk joined #isabelle
20:59 JCaesar joined #isabelle
21:43 JCaesar joined #isabelle

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