Publikationen

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
Weiterführende Links
- Personenseiten
  
  Christiansen, Jan
- Profilbereich
  
  Informatik und Gestaltung
- Fachbereich
  
  Fachbereich 3: Information und Kommunikation
Filter Tags
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
Weiterführende Links
- Personenseiten
  
  Christiansen, Jan
- Fachbereich
  
  Fachbereich 3: Information und Kommunikation
Filter Tags
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
Weiterführende Links
- Personenseiten
  
  Christiansen, Jan
- Fachbereich
  
  Fachbereich 3: Information und Kommunikation
Filter Tags
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
Weiterführende Links
- Personenseiten
  
  Christiansen, Jan
- Fachbereich
  
  Fachbereich 3: Information und Kommunikation
Filter Tags
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
Weiterführende Links
- Personenseiten
  
  Christiansen, Jan
- Fachbereich
  
  Fachbereich 3: Information und Kommunikation
Filter Tags
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
Weiterführende Links
- Personenseiten
  
  Christiansen, Jan
- Fachbereich
  
  Fachbereich 3: Information und Kommunikation
Filter Tags
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
Weiterführende Links
- Personenseiten
  
  Christiansen, Jan
- Fachbereich
  
  Fachbereich 3: Information und Kommunikation
Filter Tags
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
Weiterführende Links
- Personenseiten
  
  Christiansen, Jan
- Fachbereich
  
  Fachbereich 3: Information und Kommunikation
Filter Tags
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
Weiterführende Links
- Personenseiten
  
  Christiansen, Jan
Filter Tags
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
Weiterführende Links
- Personenseiten
  
  Christiansen, Jan
- Fachbereich
  
  Fachbereich 3: Information und Kommunikation
Filter Tags

Publikationen

Abstract

Exportformate

Weiterführende Links

Filter Tags

Exportformate

Weiterführende Links

Filter Tags

Abstract

Exportformate

Weiterführende Links

Filter Tags

Abstract

Exportformate

Weiterführende Links

Filter Tags

Exportformate

Weiterführende Links

Filter Tags

Abstract

Exportformate

Weiterführende Links

Filter Tags

Exportformate

Weiterführende Links

Filter Tags

Abstract

Exportformate

Weiterführende Links

Filter Tags

Abstract

Exportformate

Weiterführende Links

Filter Tags

Abstract

Exportformate

Weiterführende Links

Filter Tags