# Our Vision

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:

• Jesper Bengtson and Joachim Parrow used Nominal Isabelle to verify the theory of the pi-calculus. They formalised the proof that bisimulation is a congruence (both for late and early operational semantics) available here. Moreover they formalised the proof that all late bisimilar processes are early bisimilar. The corresponding papers were presented at FOSSACS'07 and SOS'07. They also used Nominal Isabelle to formalise their work on Psi-calculi, available here. This was presented at LICS 2009 and LICS 2010. Jesper finished his PhD about this in 2010 with a large formalisation in Nominal Isabelle. He also formalised CCS (here). All formalisations are part of the AFP.
• Sam Tobin-Hochstadt, a student of Matthias Felleisen, used Nominal Isabelle to formalise their work on Typed Scheme. This was presented at POPL'08.
• Lucas Dixon, Alan Smaill and Alan Bundy used Nominal Isabelle to formalise proof terms of ILL and studied proof planning with this formalisation (EDI-INF-RR-0786).
• Temesghen Kahsai and Marino Miculan formalised the spi-calculus using our work - see here.
• Ayesha Yasmeen, a student of Elsa Gunter, formalised an extension of the ambient calculus using Nominal Isabelle. This was presented in the Emerging Trends section of TPHOLs'08.
• Christian Doczkal, a student of Gert Smolka, finished in 2009 his master thesis at Saarbrücken University using Nominal Isabelle. He formalised the TT-lifting technique in order to prove strong normalisation of Moggi's computational metalanguage. This is part of the AFP repository.
• Armin Heller finished his master thesis at the TU Munich in 2010 with a simple compiler verification using Nominal Isabelle.
• James Cheney formalised a number of properties of the meta-theory of mini-XQuery in Nominal Isabelle. The plan is to extend this work to full XQuery. The preliminary results appeared at CPP'11.
• Cezary Kaliszyk with input from Henk Barendregt formalised the second fixed point theorem of the lambda calculus using Nominal Isabelle 2. This work appeared at CPP'11.
• Joachim Breitner used Nominal2 for formalising Launchbury's natural semantics for lazy evaluation. This is part of the AFP.
• Larry Paulson formalised Gödel's Incompletness Theorems using Nominal2. This work appeared in the Journal of Automated Reasoning in 2015.
• Joachim Breitner proved the correctness of a GHC compiler transformation using Nominal2. This work appeared at the Haskell Symposium 2015.

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].

References