Dariusz Biernacki's home page Home Publications Students Courses


Current PhD students:

  • Tomasz Drab
    Research on reduction strategies in lambda calculi
    Co-advised with Małgorzata Biernacka
  • Piotr Polesiuk
    Research on program equivalence in higher-order programming languages
  • Mateusz Pyzik
    Research on delimited control and algebraic effects
  • Paweł Wieczorek
    Research on static analysis of concurrent imperative programs
    Co-advised with Filip Sieczkowski

Former PhD students:

  • Marek Materzok
    Control Abstraction for Layered Continuations: Semantics, Types and Implementation, 2014

Current MSc students:

  • Łukasz Dąbek
    Work on the separability theorem in a variant of the λμ-calculus
  • Łukasz Hanuszczak
    Work on formalizing optimizing transformations for Haskell
  • Mikołaj Nowak
    Work on certifying the Featherweight Java type system in Coq
  • Gabriel Sztorc
    Work on formalizing type inference for Haskell in Coq

Former MSc students:

  • Łukasz Czapliński
    The Application of Functional Programming to the Construction of a Visual Programming Environment, 2016
  • Paweł Wieczorek
    A Formalization in Coq of the Normalization-by-Evaluation Algorithm for Martin-Löf Type Theory, 2016
  • Piotr Polesiuk
    Strong Normalization of System F-bounded: A Proof by a Coercion Translation to System F, 2014
  • Wojciech Jedynak
    Operational Semantics of Ltac: A Formal Study of the Tactic Language of the Coq Proof Assistant, 2013
  • Jakub Korczyński
    The Forte Framework for Music Composition: Two EDSLs for Music Composition and Analysis, 2012
  • Maciej Piróg
    Toward a Certified Haskell Compiler: Correctness and Implementation of the Spineless Tagless G-machine Verified in the Coq Proof Assistant, 2010
  • Filip Sieczkowski
    Automated Derivation of Abstract Machines from Reduction Semantics: A Formalisation of the Refocusing Transformation in the Coq Proof System, 2010

Former BSc students:

  • Maciej Buszka
    Implementation of Static and Dynamic Semantics for a Calculus with Algebraic Effects and Handlers Using PLT Redex, 2019
  • Mateusz Lewko
    An Implementation of a ML-Family Functional Language Using the LLVM Compiler Infrastructure, 2018