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.
  
  In this paper we consider ambient effects that may occur in Haskell,
  namely partiality, errors, and tracing, in detail. We observe that,
  while proving propositions that hold for all kinds of effects is
  attractive, not all propositions of interest hold for all kinds of
  effects. Some propositions fail for certain effects because the
  usual monadic translation models call-by-name and not call-by-need. Since
  modeling the evaluation semantics of call-by-need in the presence
  of effects like partiality is complex and not necessary to prove
  propositions for a variety of effects, we identify a specific class
  of effects for which we cannot observe a difference between
  call-by-name and call-by-need. Using this class of effects we can
  prove propositions for all effects that do not require a model of
  sharing.
  

  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, language characteristics from one area
  exist in the other and vice versa. For example, the concepts of
  non-deterministic choice and call-time choice as known from
  functional logic programming are related to and coincide with
  stochastic memoization and probabilistic choice in probabilistic
  programming, respectively.

  We will further 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 and can
  even compete with full-blown probabilistic programming languages,
  which we illustrate by several benchmarks. Under consideration in
  Theory and Practice of Logic Programming (TPLP).
  

  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.
  
  To prove properties about a Haskell function in Coq, Mona has to
  translate the function into Coq code. As Coq programs have to be
  total and Haskell programs are often not, Mona has to model
  partiality explicitly in Coq. In her quest for a solution Mona  nds
  an ancient manuscript that explains how properties about Haskell
  functions can be proven in the proof assistant Agda by translating
  Haskell programs into monadic Agda programs. By instantiating the
  monadic program with a concrete monad instance the proof can be
  performed in either a total or a partial setting. Mona discovers
  that the proposed transformation does not work in Coq due to a
  restriction in the termination checker. In fact the transformation
  does not work in Agda anymore as well, as the termination checker in
  Agda has been improved.
  
  We follow Mona on an educational journey through the land of
  functional programming where she learns about concepts like free
  monads and containers as well as basics and restrictions of proof
  assistants like Coq. These concepts are well-known individually, but
  their interplay gives rise to a solution for Mona’s problem based on
  the originally proposed monadic tranformation that has not been
  presented before. When Mona starts to test her approach by proving a
  statement about simple Haskell functions, she realizes that her
  approach has an additional advantage over the original idea in
  Agda. Mona’s final solution not only works for a speci c monad
  instance but even allows her to prove monad-generic
  properties. Instead of proving properties over and over again for
  speci c monad instances she is able to prove properties that hold
  for all monads representable by a container-based instance of the
  free monad. In order to strengthen her con dence in the
  practicability of her approach, Mona evaluates her approach in a
  case study that compares two implementations for queues. In order to
  share the results with other functional programmers the fairy tale
is available as a literate Coq file.
  
  If you are a citizen of the land of functional programming or are at
  least familiar with its customs, had a journey that involved
  reasoning about functional programs of your own, or are just a
  curious soul looking for the next story about monads and proofs,
then this tale is for you.
  

  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.
  

  The combination of non-determinism and sorting is mostly associated
  with permutation sort, a sorting algorithm that is not very useful
  for sorting and has an awful running time. In this paper we look at
  the combination of non-determinism and sorting in a different light:
  given a sorting function, we apply it to a non-deterministic
  predicate to gain a function that enumerates permutations of the
  input list. We get to the bottom of necessary properties of the
  sorting algorithms and predicates in play as well as discuss
  variations of the modelled non-determinism.
  
  On top of that, we formulate and prove a theorem stating that no
  matter which sorting function we use, the corresponding permutation
  function enumerates all permutations of the input list. We use free
  theorems, which are derived from the type of a function alone, to
  prove the statement.