Inductive Predicates via Least Fixpoints in Higher-Order Separation Logic.

Robbert Krebbers, Luko van der Maas, Enrico Tassi

Browse the full ITP paper archive.