Nominal Techniques in Isabelle/HOL

By Christian Urban. Journal of automated reasoning, 2005

314 citations recorded by the source corpus.

Subfields: Artificial Intelligence

View Paper: https://www.semanticscholar.org/paper/5d703bcc70124f3b0a828442cf218b8af94418a6

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

1. Josef Urban
2. M. Wenzel
3. Tobias Nipkow
4. Lawrence Charles Paulson
5. John Harrison
6. Freek Wiedijk
7. Christian Szegedy
8. Xavier Leroy

Citations in the corpus

• The Isabelle Framework (2008, background): “Isabelle/HOL-Nominal [44] extends Isabelle/HOL with a unique infrastructure for defining and reasoning about languages with bound variables.”
• The Design and Implementation of Typed Scheme: From Scripts to Programs (2011, unknown): “For the proof of type soundness, we used Isabelle/HOL together with the nominalisabelle package (Urban, 2008).”
• History of Interactive Theorem Proving (2014, background): “…more general forms of recursive datatypes with infinite branching, nested and mutual recursion or dual codatatypes [Gunter, 1993; Harrison, 1995a; Berghofer and Wenzel, 1999; Blanchette et al., 2014] as well as special nominal datatypes to formalize variable binding in a natural way [Urban, 2008].”