Publikationen

2023

Embedding Functional Logic Programming in Haskell via a Compiler Plugin

Prott, K.-O. ., Teegen, F. ., & Christiansen, J. . (2023). Embedding Functional Logic Programming in Haskell via a Compiler Plugin. In Practical Aspects of Declarative Languages. Boston, MA, USA: Springer. http://doi.org/10.1017/978-3-031-24841-2_3

Abstract

We present a technique to embed a functional logic language in Haskell using a GHC plugin. Our approach is based on a monadic lifting that models the functional logic semantics explicitly. Using a GHC plugin, we get many language extensions that GHC provides for free in the embedded language. As a result, we obtain a seamless embedding of a functional logic language, without having to implement a full compiler. We briefly show that our approach can be used to embed other domain-specific languages as well. Furthermore, we can use such a plugin to build a full blown compiler for our language.
Suche auf Google Scholar

DOI Verweis
Exportformate

BibTeX

EndNote X3 XML

EndNote 7 XML

EndNote tagged

RIS
Weiterführende Links
Personenseiten

Christiansen, Jan

Profilbereich

Informatik und Gestaltung

Fachbereich

Fachbereich 3: Information und Kommunikation
Filter Tags
2023

Conference Paper

Kai-Oliver Prott

Finn Teegen

Jan Christiansen

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

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

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

2013

A Semantics for Weakly Encapsulated Search in Functional Logic Programs

Christiansen, J. ., Hanus, M. ., Reck, F. ., & Seidel, D. . (2013). A Semantics for Weakly Encapsulated Search in Functional Logic Programs. In Proceedings of the 15th Symposium on Principles and Practice of Declarative Programming - PPDP 13 (S. 49–60). ACM Press. http://doi.org/10.1145/2505879.2505896

Abstract

Encapsulated search is a key feature of (functional) logic languages. It allows the programmer to access and process different results of a non-deterministic computation within a program. Unfortunately, due to advanced operational features (lazy evaluation, partial values, infinite structures), there is no straightforward definition of the semantics of encapsulated search in functional logic languages. As a consequence, various proposals and implementations are available but a rigorous definition covering all semantical aspects does not exist. In this paper, we analyze the requirements of encapsulated search in a functional logic language like Curry and provide a comprehensive definition that covers weak encapsulation, a modular form of encapsulation, as well as nested applications of search operators. We set up a denotational semantics that distinguishes non-termination and different levels of failures in a computation. The semantics is also the basis of a practical implementation of search operators in the functional logic language Curry.
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
2013

Conference Paper

Jan Christiansen

Michael Hanus

Fabian Reck

Daniel Seidel

2011

Sloth – a Tool for Checking Minimal-Strictness

Christiansen, J. . (2011). Sloth – a Tool for Checking Minimal-Strictness. In R. . Rocha & J. . Launchbury (Hrsg.), Practical Aspects of Declarative Languages (S. 160–174). Springer Berlin Heidelberg.

Abstract

We present a light-weight tool called Sloth which assists programmers in identifying unnecessarily strict first order functions. Sloth reports counterexamples in form of a partial value, the corresponding result of the tested function and a recommended result. We present examples where the hints reported by Sloth can be used to improve a function with respect to memory behaviour, non-termination, and performance in the context of functional-logic programming. Furthermore we give an example-driven introduction into the basics of the implementation of Sloth. To improve the results in comparison to an existing approach we use additional constraints to assure that Sloth s suggestions are implementable without employing parallelism.
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
2011

Conference Paper

Jan Christiansen

Ricardo Rocha

John Launchbury
Minimally Strict Polymorphic Functions

Christiansen, J. ., & Seidel, D. . (2011). Minimally Strict Polymorphic Functions. In Proceedings of the 13th International ACM SIGPLAN Symposium on Principles and Practices of Declarative Programming - PPDP 11 (S. 53). ACM Press. http://doi.org/10.1145/2003476.2003487

Abstract

In this paper we show how to efficiently check whether a polymorphic function is minimally strict. A function is minimally strict if it is the minimal element of a specific less-strict ordering. We prove that we can check whether two polymorphic functions are related by the less-strict ordering by either checking it a) for an arbitrary monomorphic instance of the functions or b) for all shapes of the functions’ argument type. A shape is a value of a monomorphic instance of a polymorphic data type where each polymorphic component is replaced by an element that identifies its position in the data structure. In contrast to recent publications that characterize polymorphic functions by monomorphic instances we consider non-termination and selective strictness, i.e., a language closer to Haskell.
Suche auf Google Scholar

DOI Verweis
Exportformate

BibTeX

EndNote X3 XML

EndNote 7 XML

EndNote tagged

RIS
Weiterführende Links
Personenseiten

Christiansen, Jan
Filter Tags
2011

Conference Paper

Jan Christiansen

Daniel Seidel

2023

Abstract

Exportformate

Weiterführende Links

Filter Tags

2020

Exportformate

Weiterführende Links

Filter Tags

2019

Abstract

Exportformate

Weiterführende Links

Filter Tags

Abstract

Exportformate

Weiterführende Links

Filter Tags

Exportformate

Weiterführende Links

Filter Tags

2018

Abstract

Exportformate

Weiterführende Links

Filter Tags

2016

Exportformate

Weiterführende Links

Filter Tags

2013

Abstract

Exportformate

Weiterführende Links

Filter Tags

2011

Abstract

Exportformate

Weiterführende Links

Filter Tags

Abstract

Exportformate

Weiterführende Links

Filter Tags