Homer: A Higher-Order Observational Equivalence Model checkER
Abstract elided by the publisher.
Related papers
- Hector: An Equivalence Checker for a Higher-Order Fragment of ML CAV 2012
- On contract satisfaction in a higher-order world TOPLAS 2011
- A relational modal logic for higher-order stateful ADTs POPL 2010
- Modeling Reachability Types with Logical Relations: Semantic Type Soundness, Termination, Effect Safety, and Equational Theory OOPSLA 2025
- Internalizing Indistinguishability with Dependent Types POPL 2024
- Abstract Operational Methods for Call-by-Push-Value POPL 2025
- A Type System Equivalent to a Model Checker ESOP 2005
- Modular verification of higher-order methods with mandatory calls specified by model programs OOPSLA 2007