Tuesday, May 17, 2011
N
Well, it took longer than expected but N is now open source! You can download it from GitHub at the URL in the previous post. Just a warning that it is buggy as hell and very fragile...
Monday, May 02, 2011
The N PL semantics tool, and other stuff
What have I been up to? I am currently gainfully unemployed. I am climbing a lot and seeing more of NZ. I'm also still working on some acadmic things - I'm continuing to work on a wildcards paper and I'm the PC chair for IWACO 11 which is keeping me busy (by the way I think this year's IWACO will be excellent - we've got a whole bunch of great submissions, thanks to everyone who submitted!).
Most excitingly (for me) I've been working on a tool for PL researchers called N. It is kind of a proof assistant, but also checks formal type systems and outputs them in pretty LaTeX, so takes out a lot of the drudgery of writing formal type systems. It is very much work in progress, but most of the checking and LaTeX output stuff is done (for a fairly small formal lanaguage) and I am working on the proof assistant part. This is novel (and exiciting for me to work on) because it is purely syntactic and high level, as opposed to Coq, Isabelle etc. which are semantic and low level, http://www.blogger.com/img/blank.gifi.e., they work at the level of logic/maths, whereas N works at the level of PL-style type systems. This means that when N says a proof is done it does not guarantee that the proof is correct. However, writing proofs in N should be orders of magnitude simpler and quicker than using a proper proof assistant. Think of it as a tool for doing hand-written proofs - it does some checking and automates some parts, but does not fully check.
N is written in Python and will be open source very soon (next few days), it will be at https://github.com/nick29581/N. Feedback is appreciated!
Most excitingly (for me) I've been working on a tool for PL researchers called N. It is kind of a proof assistant, but also checks formal type systems and outputs them in pretty LaTeX, so takes out a lot of the drudgery of writing formal type systems. It is very much work in progress, but most of the checking and LaTeX output stuff is done (for a fairly small formal lanaguage) and I am working on the proof assistant part. This is novel (and exiciting for me to work on) because it is purely syntactic and high level, as opposed to Coq, Isabelle etc. which are semantic and low level, http://www.blogger.com/img/blank.gifi.e., they work at the level of logic/maths, whereas N works at the level of PL-style type systems. This means that when N says a proof is done it does not guarantee that the proof is correct. However, writing proofs in N should be orders of magnitude simpler and quicker than using a proper proof assistant. Think of it as a tool for doing hand-written proofs - it does some checking and automates some parts, but does not fully check.
N is written in Python and will be open source very soon (next few days), it will be at https://github.com/nick29581/N. Feedback is appreciated!
Subscribe to:
Posts (Atom)