Safety and Conservativity of Definitions in Higher-Order Logic and Isabelle/HOL

Watch a conference presentation from POPL 2018 exploring the fundamental properties of definitions in Higher-Order Logic (HOL) and Isabelle/HOL theorem provers. Learn how safety and conservativity are proven for HOL definitions, which are crucial for ensuring consistency in interactive theorem proving and certified functional programming. Examine unique HOL features like non-emptiness proofs for type definitions and their implications for safety properties. Discover how this research advances beyond previous work that only demonstrated consistency of Isabelle/HOL definitions, with detailed analysis of how definitions can be treated as abbreviations while maintaining provability in the pure logic system.