We are working on a major overhaul of Nominal Isabelle. The
latest bundles of Nominal2 are
here.
We are working on a major overhaul of Nominal Isabelle. The
latest bundles of Nominal2 are
here.
To root out bugs, every programming language should be designed with the help of a theorem prover, and every compiler should be verified. With our work we aim to provide all proving technologies necessary for reasoning conveniently about programming languages (for example the lambda calculus) and compilers. For us, formal proofs should be as easy to perform as informal "pencil-and-paper" proofs - at least the overhead of formal proofs should not prevent any formalisation. Many ideas for our work come from the nominal logic work by Andrew Pitts. Our theoretical results about nominal theories enabled us to implement Nominal Isabelle on top of Isabelle/HOL.
If you want to see a simple example illustrating our results on Nominal Isabelle click here. For more interesting results, we already completed formalisations of Church-Rosser and strong-normalisation proofs as well as the first part of the PoplMark Challenge. We also formalised some typical proofs from SOS, Karl Crary's chapter on logical relations from Advanced Topics in Types and Programming Languages, and also a paper on LF by Harper and Pfenning. In the latter paper we found a gap in the soundness proof and corrected it (we actually gave three solutions to the problem [6]). Urban formalised and also corrected the main result of his PhD, a logical relation argument for establishing strong normalisation of cut-elimination in classical logic. Other people have used Nominal Isabelle too - see our list of users and projects here
Note, however, that Nominal Isabelle is still an ongoing research project, which needs both theoretical and implementation work. You are encouraged to subscribe to the (moderated) mailing list to hear about our progress and to give us feedback.
We have recently re-implemented the underlying nominal theory [7] and also have a good proposal for how to deal with general binding structures in Nominal Isabelle [8].
| [1] | Nominal Reasoning Techniques in Isabelle/HOL. In Journal of Automatic Reasoning, Vol. 40(4), 327-356, 2008. [pdf]. The predecessor paper, which appeaerd at CADE in 2005, received the Thoralf Skolem Award. |
| [2] | A Formal Treatment of the Barendregt Variable Convention in Rule Inductions (Christian Urban and Michael Norrish) Proceedings of the ACM Workshop on Mechanized Reasoning about Languages with Variable Binding and Names (MERLIN 2005), Pages 25-32, 2005. © ACM, Inc. [ps] [pdf] |
| [3] | A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL (Christian Urban and Stefan Berghofer) Proceedings of the 3rd International Joint Conference on Automated Deduction (IJCAR 2006). In volume 4130 of Lecture Notes in Artificial Intelligence, Pages 498-512, 2006. © Springer Verlag [ps] |
| [4] | A Head-to-Head Comparison of de Bruijn Indices and Names. (Stefan Berghofer and Christian Urban) Proceedings of the International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2006), ENTCS, Pages 53-67, 2006. [ps] |
| [5] | Barendregt's Variable Convention in Rule Inductions. (Christian Urban, Stefan Berghofer and Michael Norrish) Proceedings of the 21th Conference on Automated Deduction (CADE 2007). In volume 4603 of Lecture Notes in Artificial Intelligence, Pages 35-50, 2007. © Springer Verlag [ps] |
| [6] | Mechanising the Metatheory of LF. (Christian Urban, James Cheney and Stefan Berghofer) In Proc. of the 23rd IEEE Symposium on Logic in Computer Science (LICS 2008), IEEE Computer Society, Pages 45-56, 2008. [pdf] More information elsewhere. |
| [7] | Proof Pearl: A New Foundation for Nominal Isabelle. (Brian Huffman and Christian Urban) In Proc. of the 1st Conference on Interactive Theorem Proving (ITP 2010). In volume 6172 in Lecture Notes in Computer Science, Pages 35-50, 2010. [pdf] |
| [8] | General Bindings and Alpha-Equivalence in Nominal Isabelle. (Christian Urban and Cezary Kaliszyk) In Proc. of the 20th European Symposium on Programming (ESOP 2011). In Volume 6602 of Lecture Notes in Computer Science, Pages 480-500, 2011. [pdf] (and a longer version appeared in the Journal of Logical Methods in Computer Science, Volume 8 (2:14), 2012 [pdf]) |