Lista publikacji

2017

  • Ricciotti, W., Stolarek, J., Perera, R. and Cheney, J.: Imperative Functional Programs that Explain their Work, przyjęte na International Conference on Functional Programming 2017, Oksford, Wielka Brytania, wersja wstępna (pdf), repozytorium na GitHubie
    Streszczenie: Program slicing provides explanations that illustrate how program outputs were produced from inputs. We build on an approach introduced in prior work, where dynamic slicing was defined for pure higher-order functional programs as a Galois connection between lattices of partial inputs and partial outputs. We extend this approach to imperative functional programs that combine higher-order programming with references and exceptions. We present proofs of correctness and optimality of our approach and a proof-of-concept implementation and experimental evaluation.

2015

  • Stolarek, J., Peyton Jones, S. and Eisenberg, R. A.: Injective Type Families for Haskell, ACM SIGPLAN Notices 50(12):118-128 (pierwotnie wygłoszone na ACM SIGPLAN Haskell Symposium 2015, Vancouver, Kanada), wersja online (pdf), wersja rozszerzona (pdf), wystąpienie (Youtube), slajdy (pdf), DOI: 10.1145/2804302.2804314, cytowanie (BibTeX)
    Streszczenie: Haskell, as implemented by the Glasgow Haskell Compiler (GHC), allows expressive type-level programming. The most popular type-level programming extension is TypeFamilies, which allows users to write functions on types. Yet, using type functions can cripple type inference in certain situations. In particular, lack of injectivity in type functions means that GHC can never infer an instantiation of a type variable appearing only under type functions.
    In this paper, we describe a small modification to GHC that allows type functions to be annotated as injective. GHC naturally must check validity of the injectivity annotations. The algorithm to do so is surprisingly subtle. We prove soundness for a simplification of our algorithm, and state and prove a completeness property, though the algorithm is not fully complete.
    As much of our reasoning surrounds functions defined by a simple pattern-matching structure, we believe our results extend beyond just Haskell. We have implemented our solution on a branch of GHC and plan to make it available to regular users with the next stable release of the compiler.

2014

  • Eisenberg, R. A., and Stolarek, J.: Promoting Functions to Type Families in Haskell, ACM SIGPLAN Notices 49(12):95-106 (pierwotnie wygłoszone na ACM SIGPLAN Haskell Symposium 2014, Göteborg, Szwecja), wersja online (pdf), wersja rozszerzona (pdf), wystąpienie (Youtube), slajdy (pdf), DOI: 10.1145/2633357.2633361, repozytorium na GitHubie, cytowanie (BibTeX)
    Streszczenie: Haskell, as implemented in the Glasgow Haskell Compiler (GHC), is enriched with many extensions that support type-level programming, such as promoted datatypes, kind polymorphism, and type families. Yet, the expressiveness of the type-level language remains limited. It is missing many features present at the term level, including case expressions, anonymous functions, partially-applied functions, and let expressions. In this paper, we present an algorithm - with a proof of correctness - to encode these term-level constructs at the type level. Our approach is automated and capable of promoting a wide array of functions to type families. We also highlight and discuss those term-level features that are not promotable. In so doing, we offer a critique on GHC's existing type system, showing what it is already capable of and where it may want improvement. We believe that delineating the mismatch between GHC's term level and its type level is a key step toward supporting dependently typed programming.
    We have implemented our approach as part of the singletons package, available online.

2013

  • Stolarek, J.: Verifying weight biased leftist heaps using dependent types, nieopublikowane, wersja online (pdf), kod (tar.gz), repozytorium na GitHubie
    Streszczenie: This paper is an intermediate level tutorial on verification using dependent types in Agda. It is also a case study of weight biased leftist heap data structure in a purely functional, dependently typed setting. Paper demonstrates how to write a formally verified implementation that is guaranteed to maintain that structure’s invariants. The reader will learn how to construct complex equality proofs by building them from smaller parts. This knowledge will enable the reader to understand more advanced verification techniques, eg. equational reasoning provided by Agda’s standard library or tactics system found in Idris and Coq programming languages.

2012

  • Stolarek, J.: Understanding Basic Haskell Error Messages, The Monad.Reader 20, 2012, wersja online (pdf), cytowanie (BibTeX)
    Streszczenie: Haskell is a language that differs greatly from the mainstream languages of today. An emphasis on pure functions, a strong typing system, and a lack of loops and other conventional features make it harder to learn for programmers familiar only with imperative programming. One particular problem I faced during my initial contact with Haskell was unclear error messages. Later, seeing some discussions on #haskell, I noticed that I wasn't the only one. Correcting a program without understanding error messages is not an easy task. In this tutorial, I aim to remedy this problem by explaining how to understand Haskell's error messages. I will present code snippets that generate errors, followed by explanations and solutions. I used GHC 7.4.1 and Haskell Platform 2012.2.0.0 for demonstration. I assume reader's working knowledge of GHCi. I also assume that reader knows how data types are constructed, what type classes are and how they are used. Knowledge of monads and language extensions is not required.
  • Stolarek, J.: Adaptive wavelet synthesis for improving digital image watermarking, In: Towards Modern Collaborative Knowledge Sharing Systems, Springer, 133–144, Eds: Lipiński, P., and Świrski, K., 2012, wersja online (pdf), cytowanie (BibTeX)
    Streszczenie: Discrete Wavelet Transform is one of the most popular tools of digital signal processing. Many different wavelet functions have been proposed so far, however there is no wavelet that would be the most suitable for every task. Therefore a method allowing to adaptively synthesize the most suitable wavelet for a given task must be developed. In this paper a general outline of such method will be discussed. A concept of tools used for analysis of adaptive wavelets will be presented.
  • Stolarek, J., and Lipiński, P.: Improving watermark resistance against removal attacks using orthogonal wavelet adaptation, 38th Conference on Current Trends in Theory and Practice of Computer Science, volume 7147, Springer, 588–599, 2012, wersja online (pdf),cytowanie (BibTeX)
    Streszczenie: This paper proposes a new approach for enhancing the robustness of wavelet-based image watermarking algorithms. The method adjusts wavelet used in the process of image watermarking in order to maximize resistance against image processing operations. Effectiveness of the approach is demonstrated using blind multiplicative watermarking algorithm, but it can easily be generalized to all wavelet-based watermarking algorithms. Presented results demonstrate that wavelets generated using proposed approach outperform other wavelet bases commonly used in image watermarking in terms of robustness to removal attacks.

2011

  • Stolarek, J., and Byczkowska-Lipińska, L.: Wavelet adaptation based on signal processing outcome, System Modelling and Control 2011, wersja online (pdf), cytowanie (BibTeX)
    Streszczenie: The problem of wavelet synthesis is a crucial part of wavelet theory. In this paper an overview of wavelet synthesis methods used in the literature up till now is given. It is demonstrated that these well known approaches suffer from some major drawbacks. A new approach to adaptive wavelet synthesis that overcomes these drawbacks and has not been exploited before is proposed. This approach is based on adapting wavelet to one particular signal and specific signal processing algorithm.
  • Stolarek, J.: Adaptive synthesis of a wavelet transform using fast neural network, Bulletin of Polish Academy of Sciences. Technical Sciences 59(1), 2011, wersja online (pdf), cytowanie (BibTeX)
    Streszczenie: This paper introduces a new method for adaptive synthesis of a wavelet transform using fast neural network with topology based on lattice structure. Lattice structure and orthogonal lattice structure are presented and their properties are discussed. A novel method for unsupervised training of the neural network is introduced. Proposed approach is tested by synthesizing new wavelets with expected energy distribution between low- and high-pass filters. Energy compaction of proposed method and Daubechies wavelets is compared. Tests are performed using sound and image signals.
  • Stolarek, J.: On the properties of a lattice structure for a wavelet filter bank implementation: Part II, Journal of Applied Computer Science 19(2), 125-139, 2011, wersja online (pdf), cytowanie (BibTeX)
    Streszczenie: This paper continues discussion of a lattice structure for parametrization and implementation of a Discrete Wavelet Transform. Based on an algorithm for converting the lattice structure to a wavelet filter bank coefficients, developed in the first part of this paper, second part of the proof demonstrating that filters implemented by the lattice structure fulfil conditions imposed on an orthogonal wavelet filter bank is carried out.
  • Stolarek, J.: On the properties of a lattice structure for a wavelet filter bank implementation: Part I, Journal of Applied Computer Science 19(1), 85-116, 2011, wersja online (pdf), cytowanie (BibTeX)
    Streszczenie: This paper presents concept of a lattice structure for parametrization and implementation of a Discrete Wavelet Transform. Theoretical properties of the lattice structure are discussed in detail. An algorithm for converting the lattice structure to a wavelet filter bank coefficients is constructed. A theoretical proof demonstrating that filters implemented by the lattice structure fulfil conditions imposed on an orthogonal wavelet filter bank is conducted.
  • Lipiński, P., and Stolarek, J.: Digital watermarking enhancement using wavelet filter parametrization, Adaptive and Natural Computing Algorithms (10th ICANNGA, 2011), volume 1, 330-339, Eds: Dobnikar, A., Lotrič, U., and Šter, B., 2011, wersja online (pdf), cytowanie (BibTeX)
    Streszczenie: In this paper a genetic-based enhancement of digital image watermarking in the Discrete Wavelet Transform domain is presented. The proposed method is based on adaptive synthesis of a mother wavelet used for image decomposition. Wavelet synthesis is performed using parametrization based on an orthogonal lattice structure. A genetic algorithm is applied as an optimization method to synthesize a wavelet that provides the best watermarking quality in respect to the given optimality criteria. Effectiveness of the proposed method is demonstrated by comparing watermarking results using synthesized wavelets and the most commonly used Daubechies wavelets. Experiments demonstrate that mother wavelet selection is an important part of a watermark embedding process and can influence watermarking robustness, separability and fidelity.

2010

  • Stolarek, J.: Adaptive wavelet synthesis for improving digital image processing, 1st TEWI Conference, 2010, prezentacja (pdf), cytowanie (BibTeX)
    Streszczenie: Discrete Wavelet Transform is one of the most popular tools of digital signal processing. Many different wavelet functions have been proposed so far, however there is no wavelet that would be the most suitable for every task. Therefore a method allowing to adaptively synthesize the most suitable wavelet for a given task must be developed. In this paper a general outline of such method will be discussed. A concept of tools used for analysis of adaptive wavelets will be presented.
  • Stolarek, J.: Improving energy compaction of a wavelet transform using genetic algorithm and fast neural network, Archives of Control Sciences 20(4), 417-433, December 2010, wersja online (pdf), cytowanie (BibTeX)
    Streszczenie: In this paper a new method for adaptive synthesis of a smooth orthogonal wavelet, using fast neural network and genetic algorithm, is introduced. Orthogonal lattice structure is presented. A new method of supervised training of fast neural network is introduced to synthesize a wavelet with desired energy distribution between output signals from low-pass and high-pass filters on subsequent levels of a Discrete Wavelet Transform. Genetic algorithm is proposed as a global optimization method for defined objective function, while neural network is used as a local optimization method to further improve the result. Proposed approach is tested by synthesizing wavelets with expected energy distribution between low- and high-pass filters. Energy compaction of proposed method and Daubechies wavelets is compared. Tests are performed using image signals.
  • Stolarek, J., and Lipiński, P.: Improving digital watermarking fidelity using fast neural network for adaptive wavelet synthesis, Journal of Applied Computer Science 18(1), 61-74, 2010, artykuł online (pdf), cytowanie (BibTeX)
    Streszczenie: This paper introduces a new adaptive algorithm for digital watermark embedding in wavelet domain. The proposed algorithm performs adaptive mother wavelet synthesis based on a low frequency component energy maximization. The algorithm is based on an orthogonal neural network. We demonstrate that the presented adaptive method can improve both the correlation between an extracted watermark and an embedded watermark, as well as the fidelity of an image. The proposed algorithm is applied to improve well known wavelet based embedding algorithms.

2009

  • Stolarek, J.: Synthesis of a wavelet transform using neural network, XI International PhD Workshop OWD, Conference Archives PTETiS, volume 26, 71-74, 2009, wersja online (pdf), prezentacja (pdf), cytowanie (BibTeX)
    Streszczenie: Wavelet transform has a wide area of application in signal processing. However there is no single wavelet perfectly suitable for every task. In practice Daubechies 4 is the most commonly used wavelet, since it is well suited for analysis of many natural signals and it offers a straightforward interpretation of the results. It would be very useful to develop a method for adaptive synthesis of a wavelet transform suitable for particular task. Artificial neural networks offer such ability. So far this approach wasn't explored. This paper presents neural network for synthesis of orthogonal wavelet transform and a method of unsupervised training of this network.
  • Stolarek, J., and Yatsymirskyy, M.: Fast neural network for synthesis and implementation of orthogonal wavelet transform, Image Processing & Communications Challenges, AOW EXIT, 87-94, 2009, wersja online (pdf), cytowanie (BibTeX)
    Streszczenie: This paper presents lattice structure and orthogonal lattice structure for synthesis of a wavelet transform. Lattice structure is based on parametrized 2×2 operations. Adjustment of parameter values leads to synthesis of a new wavelet transform. Fast neural network with topology based on lattice structure is applied to determine values of the parameters. Factorization-based reduction in number of arithmetic operations is demonstrated.
  • Stolarek, J.: Realization of Daubechies transform using lattice structure, The Collection of Scientific Works of ISDMCI 2009, 188-192, 2009, wersja online (pdf), prezentacja (pdf), cytowanie (BibTeX)
    Streszczenie: This paper presents a new approach to wavelet synthesis by using fast neural networks. Fast neural network architecture and the training process are discussed. Training results are presented showing that the proposed network is able to learn the Daubechies wavelet transform.

2008

  • Stolarek, J.: Nowe kryteria wykrywania minucji w algorytmie rozpoznawania odcisków palców, XVI Konferencja Sieci i Systemy Informatyczne. Teoria, Projekty, Wdrożenia, Aplikacje [Dokument elektroniczny], 1 dysk optyczny (CD-ROM) D:/referaty/16003.pdf s.[1-6], Łódź, Polska, 2008, wersja online (pdf), prezentacja (pdf), cytowanie (BibTeX)
    Streszczenie: W artykule przedstawiono ulepszenie algorytmu rozpoznawania użytkownika na podstawie analizy odcisków palców. Algorytm polega na śledzeniu przebiegu linii papilarnych w celu wykrycia minucji, czyli miejsc w których linie papilarne kończą się lub rozgałęziają. Autor prezentuje nowe kryteria pozwalające stwierdzić istnienie w danym punkcie minucji. Układ minucji pozwala na jednoznaczne rozpoznanie osoby.
pl/research/publications.txt · ostatnio zmienione: 2017/05/09 13:07 przez Jan Stolarek