Publikationen

Autor*in

Jahr der Veröffentlichung

Publikationsformat

Keyword

Forschungsprojekt

Institut/Einrichtung

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
Personenseiten

Christiansen, Jan

Fachbereich

Fachbereich 3: Information und Kommunikation
Filter Tags
2020

Journal Article

Sandra Dylus

Jan Christiansen

Finn Teegen

2019

Proving Inequational Propositions about Haskell Programs in Coq

Christiansen, J. ., & Dylus, S. . (2019). 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
Personenseiten

Christiansen, Jan

Fachbereich

Fachbereich 3: Information und Kommunikation
Filter Tags
2019

Unpublished

Jan Christiansen

Sandra Dylus
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

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
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

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
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

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
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
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

Publikationen

2020

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

Exportformate

Weiterführende Links

Filter Tags

2019

Proving Inequational Propositions about Haskell Programs in Coq

Exportformate

Weiterführende Links

Filter Tags

Verifying Effectful Haskell Programs in Coq

Abstract

Exportformate

Weiterführende Links

Filter Tags

One Monad to Prove Them All

Abstract

Exportformate

Weiterführende Links

Filter Tags

2018

Probabilistic Functional Logic Programming

Abstract

Exportformate

Weiterführende Links

Filter Tags

2016

All Sorts of Permutations (Functional Pearl)

Exportformate

Weiterführende Links

Filter Tags