Dariusz Biernacki's home page Home Publications Students Courses


Current PhD students:

  • Mateusz Pyzik
    Research on the operational semantics of delimited control and algebraic effects

Former PhD students:

  • Tomasz Drab
    Reduction Strategies in the Lambda Calculus and Their Implementation through Derivable Abstract Machines, 2022, submitted
    Co-advised with Małgorzata Biernacka
  • Piotr Polesiuk
    Reasoning About Control Effects: From Program Equivalence to Language Design, 2021
  • Marek Materzok
    Control Abstraction for Layered Continuations: Semantics, Types and Implementation, 2014

Current MSc students:

Former MSc students:

  • Kamil Listopad
    A Fine-Grained Evaluation Strategy for Delimited-Control Operators shift0/dollar, 2022
  • Konrad Werbliński
    Implementation of a Compiler and a Virtual Machine for a Programming Language with Algebraic Effects, 2022
    Co-advised with Filip Sieczkowski
  • Gabriel Sztorc
    Formal Verification of Type Inference for a Minimal Fragment of Haskell Using the Coq Proof Assistant, 2022
  • Maciej Buszka
    The Functional Correspondence Applied: An Implementation of a Semantics Transformer, 2020
  • Łukasz Dąbek
    Böhm's Theorem in Lambda Calculi with Control Operators, 2019
  • Mikołaj Nowak
    A Coq Formalization of a Type System for an Object-Oriented Programming Language, 2019
  • Ł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

Current BSc students:

Former BSc students:

  • Wiktor Kuchta
    Normalization for Algebraic Effect Handlers, 2022
  • 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