Skip to main content Accessibility help
×
  1. Home
  2. Journals
  3. Journal of Functional Programming
  4. Collections
  5. OOPSLA’22
Journal Home
Refine listing

Refine listing

Access:
Publication date:

Actions for selected content:

Select all | Deselect all
  • View selected items
  • Export citations
  • Download PDF (zip)
  • Save to Kindle
  • Save to Dropbox
  • Save to Google Drive

Save Search

You can save your searches here and later view and run them again in "My saved searches".

Please provide a title, maximum of 40 characters.
Cancel
×

OOPSLA’22

Contents

Research Article

  • Checking equivalence in a non-strict language

  • Part of:
  • JOHN CHARLES KOLESAR, RUZICA PISKAC, WILLIAM TRIEST HALLAHAN
  • Journal:
    Journal of Functional Programming / Volume 35 / 2025
    Published online by Cambridge University Press:
    15 September 2025, e19
    • Article
      • You have access
      • Open access
    • PDF
    • HTML
    • Export citation

  • Program equivalence checking is the task of confirming that two programs have the same behavior on corresponding inputs. We develop a calculus based on symbolic execution and coinduction to check the equivalence of programs in a non-strict functional language. Additionally, we show that our calculus can be used to derive counterexamples for pairs of inequivalent programs, including counterexamples that arise from non-termination. We describe a fully automated approach for finding both equivalence proofs and counterexamples. Our implementation, nebula, proves equivalences of programs written in Haskell. We demonstrate nebula’s practical effectiveness at both proving equivalence and producing counterexamples automatically by applying nebula to existing benchmark properties.