Publikationen

2020

• Implementing a Library for Probabilistic Programming Using Non-Strict Non-Determinism

  Dylus, S. ., Christiansen, J. ., & Teegen, F. . (2020). Implementing a Library for Probabilistic Programming Using Non-Strict Non-Determinism. Theory and Practice of Logic Programming, 20, 147–175. http://doi.org/10.1017/S1471068419000085

  • 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

  • 2020
  • Journal Article
  • • Sandra Dylus
    • Jan Christiansen
    • Finn Teegen

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

• One Monad to Prove Them All

  Dylus, S. ., Christiansen, J. ., & Teegen, F. . (2019). One Monad to Prove Them All. The Art, Science, and Engineering of Programming, 3. http://doi.org/10.22152/programming-journal.org/2019/3/8

  Abstract

  anzeigen ▸

  One Monad to Prove Them All is a modern fairy tale about curiosity and perseverance, two important properties of a successful PhD student. We follow the PhD student Mona on her adventure of proving properties about Haskell programs in the proof assistant Coq. On the one hand, as a PhD student in computer science Mona observes an increasing demand for correct software products. In particular, because of the large amount of existing software, verifying existing software products becomes more important. Verifying programs in the functional programming language Haskell is no exception. On the other hand, Mona is delighted to see that communities in the area of theorem proving are becoming popular. Thus, Mona sets out to learn more about the interactive theorem prover Coq and verifying Haskell programs in Coq.

  • 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
  • Journal Article
  • • Sandra Dylus
    • Jan Christiansen
    • Finn Teegen

2018

• Probabilistic Functional Logic Programming

  Dylus, S. ., Christiansen, J. ., & Teegen, F. . (2018). Probabilistic Functional Logic Programming. In Practical Aspects of Declarative Languages (S. 3–19). Springer International Publishing.

  Abstract

  anzeigen ▸

  This paper presents PFLP, a library for probabilistic programming in the functional logic programming language Curry. It demonstrates how the concepts of a functional logic programming language support the implementation of a library for probabilistic programming. In fact, the paradigms of functional logic and probabilistic programming are closely connected. That is, we can apply techniques from one area to the other and vice versa. We will see that an implementation based on the concepts of functional logic programming can have benefits with respect to performance compared to a standard list-based implementation.

  • Suche auf Google Scholar

  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

  • 2018
  • Conference Paper
  • • Sandra Dylus
    • Jan Christiansen
    • Finn Teegen

2016

• All Sorts of Permutations (Functional Pearl)

  Christiansen, J. ., Danilenko, N. ., & Dylus, S. . (2016). All Sorts of Permutations (Functional Pearl). In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (S. 168–179). ACM. http://doi.org/10.1145/2951913.2951949

  • 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

  • 2016
  • Conference Paper
  • • Jan Christiansen
    • Nikita Danilenko
    • Sandra Dylus
  • • free theorems
    • Haskell
    • monads
    • non-determinism
    • permutation
    • sorting

• Proving Inequational Propositions about Haskell Programs in Coq

  Christiansen, J. ., & Dylus, S. . Proving Inequational Propositions about Haskell Programs in Coq.

  • Suche auf Google Scholar

  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

  • Unpublished
  • • Jan Christiansen
    • Sandra Dylus