Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2014-01-10

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

All times shown according to UTC.

Time Nick Message
13:28 tangentstorm joined #isabelle
13:52 tangentstorm from what i can tell, it seems possible to write proofs about arbitrary languages in isar, but how would i go about it?
13:52 tangentstorm like I'm a fan of a very compact programming language called J, and i'd like to write some proofs about it.
13:53 tangentstorm for example, i wrote this: https://github.com/tangentstorm/tangentlabs/blob/master/j/umax.ijs
13:53 tangentstorm i'd like to rewrite it a more formal way.
13:54 tangentstorm is that possible with isar?
13:56 tangentstorm also i posted a little bit about it here if anyone wants to chime in making a pitch to an audience interested in formal proofs :) http://www.reddit.com/r/computingscience/comments/1uvplc/isar_a_proof_language_with_interactive_prover/
16:15 felipealmeida joined #isabelle
21:06 felipealmeida joined #isabelle

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