Publikationen

2019

• Verifying Effectful Haskell Programs in Coq

  Christiansen, J., Dylus, S., & Bunkenburg, N. (2019). Verifying Effectful Haskell Programs in Coq. In Proceedings of the 12th ACM SIGPLAN International Symposium on Haskell - Haskell 2019 (S. 125-138). ACM Press. http://doi.org/10.1145/3331545.3342592

  Abstract

  anzeigen ▸

  We show how various Haskell language features that are related to ambient effects can be modeled in Coq. For this purpose we build on previous work that demonstrates how to reason about existing Haskell programs by translating them into monadic Coq programs. A model of Haskell programs in Coq that is polymorphic over an arbitrary monad results in non-strictly positive types when transforming recursive data types likes lists. Such non-strictly positive types are not accepted by Coq’s termination checker. Therefore, instead of a model that is generic over any monad, the approach we build on uses a specific monad instance, namely the free monad in combination with containers, to model various kinds of effects. This model allows effect-generic proofs.

  • Suche auf Google Scholar
  • DOI Verweis

  Exportformate

  • BibTeX
  • EndNote X3 XML
  • EndNote 7 XML
  • EndNote tagged
  • RIS

  Weiterführende Links

  anzeigen ▸

  • Personenseiten

    • Christiansen, Jan

  • Fachbereich

    • Fachbereich 3: Information und Kommunikation

  Filter Tags

  • 2019
  • Conference Paper
  • • Jan Christiansen
    • Sandra Dylus
    • Niels Bunkenburg