Users of Nominal Isabelle

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:

PhD Theses using Nominal Isabelle

• Jesper Bengtson (now professor at ITU in Copenhagen) finished his PhD in 2010 with a large formalisation of the Psi-Calculus in Nominal Isabelle (see here). The Psi-calculus is a parametric framework for reasoning about process calculi. He also formalised CCS (here) using Nominal Isabelle.

Journal and Conference Papers using Nominal Isabelle

• 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. 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 and is part of the AFP.
• Larry Paulson formalised a second Part of Gödel's Incompletness Theorems using Nominal2. This is part of the AFP.
• Joachim Breitner proved the correctness of a GHC compiler transformation using Nominal2. This work appeared at the Haskell Symposium 2015.
• Matthias Brun and Dmitriy Traytel formalised Generic Authenticated Data Structures using Nominal Isabelle. The AFP entry is here. This work appeared in the Proceedings of the International Conference on Concurrency Theory (CONCUR 2015).
• Tjark Weber et al formalise a uniform semantic substrate for a wide variety of process calculi where states and action labels can be from arbitrary nominal sets. This includes a Hennessy-Milner logic for these systems. The AFP entry is here. This work appeared in the Proceedings of the International Conference on Concurrency Theory (CONCUR 2015).
• Andrei Popescu and Dmitriy Traytel gave a Formally Verified Abstract Account of Gödel's Incompleteness Theorems using Nominal Isabelle. The AFP entries are here, here and here. This work appeared in the Proceedings of the International Conference on Automated Deduction (CADE 2019).
• Matthias Brun and Dmitriy Traytel formalised Generic Authenticated Data Structures using Nominal Isabelle. The AFP entry is here. This work appeared in the Proceedings of International Conference on Interactive Theorem Proving (ITP 2019).
• Andrei Popescu and Dmitriy Traytel formalise Robinson Arithmetic. This includes unary term-for-var substitution for two syntactic categories (terms and formulas) and proves 15 delicate theorems: compositionality of substitution w.r.t. itself, freshness, constructors. The AFP entry is here. This work appeared in the Proceedings of the International Conference on Automated Deduction (CADE 2019).

Entries in the Archive of Formal Proofs (AFP) using Nominal Isabelle

• Joachim Breitner proved the correctness of a GHC compiler transformation using Nominal2. The AFP entry is here. This work appeared at the Haskell Symposium 2015.
• Mark Wassell, Alasdair Armstrong, Neel Krishnaswami and Peter Sewell mechanised the Metatheory for the MiniSail ISA Specification Language using Nominal Isabelle. They needed Nominal Isabelle for handling binding. The AFP entry is here. This work appeared in the Proceedings of the 48th International Symposium on Microarchitecture MICRO-48 (2015) and at the Automated Reasoning Workshop (ARW 2018).
• Bertram Felgenhauer et al formalise the Z property introduced by Dehornoy and van Oostrom using Nominal 2. The AFP entry is here.

Entries in the Archive of Formal that had to work around the current limitations of Nominal

• Bertram Felgenhauer formalised a higher-order term algebra, generalizing the notions of free variables, matching, and substitution. The Nominal framework provides support for reasoning over fresh names, but unfortunately, its definitions are not executable. The AFP entry is here.

[Validate this page.]